Ugly commit.

prusti-contracts/prusti-contracts/src/lib.rs

@@ -176,6 +176,12 @@ mod private {
     /// not allow it. It should not be possible to construct from Rust code,
     /// hence the private unit inside.
     pub struct Lifetime(());
+
+    /// A methematical type representing a machine byte.
+    pub struct Byte(());
+
+    /// A methematical type representing a sequence of machine bytes.
+    pub struct Bytes(());
 }
 
 #[cfg(feature = "prusti")]
@@ -374,6 +380,14 @@ mod private {
             panic!()
         }
     }
+
+    /// A methematical type representing a machine byte.
+    #[derive(Copy, Clone, PartialEq, Eq)]
+    pub struct Byte(());
+
+    /// A methematical type representing a sequence of machine bytes.
+    #[derive(Copy, Clone, PartialEq, Eq)]
+    pub struct Bytes(());
 }
 
 /// This function is used to evaluate an expression in the context just
@@ -576,6 +590,28 @@ macro_rules! own_range {
     };
 }
 
+/// Obtain the bytes of the specified memory block.
+#[doc(hidden)]
+#[trusted]
+pub fn prusti_bytes<T>(_address: T, _length: usize) -> Bytes {
+    unreachable!();
+}
+
+#[macro_export]
+macro_rules! bytes {
+    ($address:expr, $length:expr) => {
+        $crate::prusti_bytes(unsafe { core::ptr::addr_of!($address) }, $length)
+    };
+}
+
+/// Read the byte at the given index.
+///
+/// FIXME: This function does not check bounds. Instead, it returns garbage in
+/// case of out-of-bounds
+pub fn read_byte(bytes: Bytes, index: Int) -> Byte {
+    unreachable!();
+}
+
 /// Indicates that we have the `raw` capability to the specified address.
 #[doc(hidden)]
 #[trusted]