trusted chunk crate

libs/trusted_chunk/.gitignore

@@ -0,0 +1,2 @@
+target
+.vscode

libs/trusted_chunk/Cargo.toml

@@ -0,0 +1,14 @@
+[package]
+name = "trusted_chunk"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+prusti-contracts = "^0.1"
+cfg-if = "1.0.0"
+range_inclusive = {git = "https://github.com/Ramla-I/range_inclusive"}
+spin = "0.9.4"
+
+[features]
+default = []
+std = []

libs/trusted_chunk/README.md

@@ -0,0 +1,22 @@
+# trusted_chunk
+This crate contains a TrustedChunk type with verified methods that prevent creating chunks with overlapping ranges.
+This is done by storing information about all previously created chunks in a verified bookkeeping data structure (an array before heap initialization and a linked list after). A TrustedChunkAllocator stores the bookkeeping structures and provides the only public interface to create a TrustedChunk. All chunks created from a single TrustedChunkAllocator instance do not overlap.
+
+## Running Prusti on this crate
+1. Download the pre-compiled binary for Release v-2023-01-26 from [here](https://github.com/viperproject/prusti-dev/releases/tag/v-2023-01-26-1935)
+2. Navigate to the prusti-release folder
+3. Run this command 
+```
+./prusti-rustc <path to trusted_chunk/src/lib.rs> -Pcheck_overflows=false --crate-type=lib --cfg "prusti" --cfg "std"
+```
+
+## Notes for Prusti improvements
+1. Eq, PartialEq, Ord, etc. traits should be pure by default
+2. Functions for structs with generics lead to internal compiler errors
+
+## Working with cargo-prusti
+We can also use the cargo-prusti tool by running it in the repo with the Cargo.toml file, and adding a Prusti.toml file with the prusti flags.
+We would also have to change the syntax for conditional compilation in the crate to [cfg(feature = "prusti")]
+```
+./<path>/cargo-prusti  --features prusti
+```

libs/trusted_chunk/src/external_spec/mod.rs

@@ -0,0 +1,9 @@
+//! The external spec files are specifications of commonly used types like `Option`, `Vec` and `RangeInclusive`.
+//! We also provide helper functions to peek into the values of the `Result` and `Option` types to be used in specifications.
+//! The specs are simple and easy to understand, and only the subset of functions used in the verification are specified.
+//! It is expected that type definitions given here are only used during verification, and the actual crates will be used when running the application.
+//! For that, we use conditional compilation.
+
+pub(crate) mod trusted_range_inclusive;
+pub(crate) mod trusted_option;
+pub(crate) mod trusted_result;

libs/trusted_chunk/src/external_spec/trusted_option.rs

@@ -0,0 +1,55 @@
+//! The specification for the `Option` type and helper functions to peek the inner value.
+
+use prusti_contracts::*;
+use crate::external_spec::trusted_range_inclusive::*;
+
+#[extern_spec]
+impl<T: PartialEq + Copy> core::option::Option<T> {
+    #[pure]
+    #[ensures(matches!(*self, Some(_)) == result)]
+    pub fn is_some(&self) -> bool;
+
+    #[pure]
+    #[ensures(self.is_some() == !result)]
+    pub fn is_none(&self) -> bool;
+
+    #[requires(self.is_some())]
+    #[ensures(result == peek_option(&self))]
+    pub fn unwrap(self) -> T;
+
+    #[ensures(result.is_some() ==> (old(self.is_some()) && old(peek_option(&self)) == peek_option(&result)))]
+    #[ensures(result.is_none() ==> old(self.is_none()))]
+    pub fn take(&mut self) -> Option<T>;
+}
+
+#[extern_spec]
+impl<T: Copy + PartialEq> PartialEq for core::option::Option<T> {
+    #[pure]
+    #[ensures(self.is_none() && other.is_none() ==> result == true)]
+    #[ensures(self.is_none() && other.is_some() ==> result == false)]
+    #[ensures(self.is_some() && other.is_none() ==> result == false)]
+    #[ensures(self.is_some() && other.is_some() ==> {
+        let val1 = peek_option(&self);
+        let val2 = peek_option(&other);
+        result == (val1 == val2)
+    })]
+    fn eq(&self, other:&Self) -> bool;
+}
+
+#[pure]
+#[requires(val.is_some())]
+pub(crate) fn peek_option<T: Copy>(val: &Option<T>) -> T {
+    match val {
+        Some(val) => *val,
+        None => unreachable!(),
+    }
+}
+
+#[pure]
+#[requires(val.is_some())]
+pub(crate) fn peek_option_ref<T>(val: &Option<T>) -> &T {
+    match val {
+        Some(val) => val,
+        None => unreachable!(),
+    }
+}

libs/trusted_chunk/src/external_spec/trusted_range_inclusive.rs

@@ -0,0 +1,34 @@
+//! A specification for `RangeInclusive` which is just an actual type definition and relevant functions.
+//! We don't use a Prusti external spec here because of dependency errors when using prusti-rustc (maybe due to a git path?) 
+//! and Prusti errors about the return types of pure functions and some "unexpected panics" when using cargo-prusti.
+
+use prusti_contracts::*;
+
+#[derive(Copy, Clone, PartialEq, Eq)]
+pub struct RangeInclusive<Idx: Clone + PartialOrd> {
+    start: Idx,
+    end: Idx
+}
+
+impl<Idx: Clone + PartialOrd> RangeInclusive<Idx> {
+    #[ensures(result.start == start)]
+    #[ensures(result.end == end)]
+    pub(crate) const fn new(start: Idx, end: Idx) -> Self {
+        Self{start, end}
+    }
+
+    #[pure]
+    pub const fn start(&self) -> &Idx {
+        &self.start
+    }
+
+    #[pure]
+    pub const fn end(&self) -> &Idx {
+        &self.end
+    }
+
+    pub fn is_empty(&self) -> bool {
+        !(self.start <= self.end)
+    }
+
+}

libs/trusted_chunk/src/external_spec/trusted_result.rs

@@ -0,0 +1,40 @@
+//! Helper functions for `Result` to peek the inner value.
+//! We don't have to write an extern spec for `Result` because it's already in prusti_contracts.
+
+use prusti_contracts::*;
+
+#[pure]
+#[requires(val.is_ok())]
+pub(crate) fn peek_result<T: Copy, E>(val: &Result<T,E>) -> T {
+    match val {
+        Ok(val) => *val,
+        Err(_) => unreachable!(),
+    }
+}
+
+#[pure]
+#[requires(val.is_ok())]
+pub(crate) fn peek_result_ref<T, E>(val: &Result<T,E>) -> &T {
+    match val {
+        Ok(val) => val,
+        Err(_) => unreachable!(),
+    }
+}
+
+#[pure]
+#[requires(val.is_err())]
+pub(crate) fn peek_err<T, E: Copy>(val: &Result<T,E>) -> E {
+    match val {
+        Ok(_) => unreachable!(),
+        Err(e) => *e,
+    }
+}
+
+#[pure]
+#[requires(val.is_err())]
+pub(crate) fn peek_err_ref<T, E>(val: &Result<T,E>) -> &E {
+    match val {
+        Ok(_) => unreachable!(),
+        Err(e) => e,
+    }
+}

libs/trusted_chunk/src/lib.rs

@@ -0,0 +1,49 @@
+#![cfg_attr(not(std), no_std)]
+#![feature(box_patterns)]
+#![allow(unused)]
+#![feature(step_trait)]
+#![feature(rustc_private)]
+
+#[macro_use]
+extern crate prusti_contracts;
+#[macro_use]
+extern crate cfg_if;
+extern crate core;
+
+pub(crate) mod spec;
+pub(crate) mod external_spec;
+pub mod linked_list;
+pub mod static_array;
+pub mod trusted_chunk;
+mod test;
+
+cfg_if::cfg_if! {
+if #[cfg(prusti)] {
+    use crate::external_spec::trusted_range_inclusive::*;
+} else {
+    extern crate alloc;
+    extern crate range_inclusive;
+    extern crate spin;
+    use range_inclusive::*;
+
+    static INIT: spin::Once<bool> = spin::Once::new();
+}
+}
+
+
+#[cfg(not(prusti))] // prusti can't reason about fn pointers
+pub fn init() -> Result<fn(RangeInclusive<usize>) -> trusted_chunk::TrustedChunk, &'static str> {
+    if INIT.is_completed() {
+        Err("Trusted Chunk has already been initialized and callback has been returned")
+    } else {
+        INIT.call_once(|| true);
+        Ok(create_from_unmapped)
+    }
+}
+
+#[requires(*frames.start() <= *frames.end())]
+#[ensures(result.start() == *frames.start())]
+#[ensures(result.end() == *frames.end())]
+fn create_from_unmapped(frames: RangeInclusive<usize>) -> trusted_chunk::TrustedChunk {
+    trusted_chunk::TrustedChunk::trusted_new(frames)
+}