Introduce the Kani Rust verifier

.github/workflows/push.yaml

@@ -126,10 +126,17 @@ jobs:
         uses: actions/upload-pages-artifact@v2
         with:
           path: out/html
+  check-kani-proofs:
+    name: Check Kani proofs
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+      - name: Check Kani proofs
+        run: make -C hacking/kani/docker check
   deploy-docs:
     name: Deploy docs
     if: github.ref == format('refs/heads/{0}', github.event.repository.default_branch)
-    needs: [check-dependencies, build-everything]
+    needs: [check-dependencies, build-everything, check-kani-proofs]
     permissions:
       pages: write
       id-token: write
@@ -141,12 +148,3 @@ jobs:
       - name: Deploy to GitHub Pages
         id: deployment
         uses: actions/deploy-pages@v2
-
-# NOTE
-#
-# May be necessary in the future:
-#
-
-#
-# For debugging and monitoring disk usage:
-# (make foo && df -h) || (df -h && false)

crates/sel4/bitfield-ops/src/lib.rs

@@ -15,12 +15,16 @@ pub trait UnsignedPrimInt:
     + BitOrAssign
     + Shl<usize, Output = Self>
     + Shr<usize, Output = Self>
-    + Default // HACK for generic 0
+    + From<bool> // HACK for generic 0 and 1
 {
     const NUM_BITS: usize = mem::size_of::<Self>() * 8;
 
     fn zero() -> Self {
-        Default::default()
+        false.into()
+    }
+
+    fn one() -> Self {
+        true.into()
     }
 }
 
@@ -109,6 +113,11 @@ impl<T: UnsignedPrimInt> UnsignedPrimIntExt for T {}
 
 // // //
 
+pub fn get_bit<T: UnsignedPrimInt>(src: &[T], i: usize) -> bool {
+    assert!(i < src.len() * T::NUM_BITS);
+    src[i / T::NUM_BITS] & (T::one() << (i % T::NUM_BITS)) != T::zero()
+}
+
 pub fn get_bits<T: UnsignedPrimInt, U: UnsignedPrimInt + TryFrom<T>>(
     src: &[T],
     src_range: Range<usize>,
@@ -193,6 +202,18 @@ pub fn set_bits_from_slice<T: UnsignedPrimInt, U: UnsignedPrimInt>(
 ) where
     T: TryFrom<usize>,
     usize: TryFrom<U>,
+{
+    set_bits_from_slice_via::<_, _, usize>(dst, dst_range, src, src_start)
+}
+
+fn set_bits_from_slice_via<T: UnsignedPrimInt, U: UnsignedPrimInt, V: UnsignedPrimInt>(
+    dst: &mut [T],
+    dst_range: Range<usize>,
+    src: &[U],
+    src_start: usize,
+) where
+    T: TryFrom<V>,
+    V: TryFrom<U>,
 {
     let num_bits = dst_range.len();
 
@@ -202,11 +223,11 @@ pub fn set_bits_from_slice<T: UnsignedPrimInt, U: UnsignedPrimInt>(
 
     let mut cur_xfer_start = 0;
     while cur_xfer_start < num_bits {
-        let cur_xfer_end = num_bits.min(cur_xfer_start + usize::NUM_BITS);
+        let cur_xfer_end = num_bits.min(cur_xfer_start + V::NUM_BITS);
         let cur_xfer_src_range = (src_start + cur_xfer_start)..(src_start + cur_xfer_end);
         let cur_xfer_dst_range =
             (dst_range.start + cur_xfer_start)..(dst_range.start + cur_xfer_end);
-        let xfer: usize = get_bits(src, cur_xfer_src_range);
+        let xfer: V = get_bits(src, cur_xfer_src_range);
         set_bits(dst, cur_xfer_dst_range, xfer);
         cur_xfer_start = cur_xfer_end;
     }
@@ -365,7 +386,7 @@ mod test {
     }
 
     #[test]
-    fn this_works_too() {
+    fn multiple_gets_return_what_was_set_with_multiple_sets() {
         for init in [0, !0] {
             let mut arr = Bitfield::<[u64; 1], u64>::new([init]);
             arr.set_bits::<u64>(0..2, 0b11);
@@ -377,3 +398,63 @@ mod test {
         }
     }
 }
+
+#[cfg(kani)]
+mod verification {
+    use super::*;
+
+    #[kani::proof]
+    #[kani::unwind(4)]
+    fn slice_ops() {
+        slice_ops_generic::<u64, 3, u8, 3, u8>(kani::any());
+        slice_ops_generic::<u8, 3, u64, 3, u8>(kani::any());
+        slice_ops_generic::<u64, 3, u8, 3, u32>(kani::any());
+        slice_ops_generic::<u8, 3, u64, 3, u32>(kani::any());
+    }
+
+    // The type of kani::any() can't depend on generic parameters, so we pass the arrays as args.
+    fn slice_ops_generic<T, const N: usize, U, const M: usize, V>((a, b): ([T; N], [U; M]))
+    where
+        T: UnsignedPrimInt + TryFrom<V>,
+        U: UnsignedPrimInt + TryFrom<V>,
+        V: UnsignedPrimInt + TryFrom<T> + TryFrom<U>,
+    {
+        let n: usize = kani::any();
+        let start_a: usize = kani::any();
+        let start_b: usize = kani::any();
+
+        kani::assume(n <= a.len());
+        kani::assume(n <= b.len());
+        kani::assume(
+            start_a
+                .checked_add(n)
+                .map(|end| end <= a.len())
+                .unwrap_or(false),
+        );
+        kani::assume(
+            start_b
+                .checked_add(n)
+                .map(|end| end <= b.len())
+                .unwrap_or(false),
+        );
+
+        let range_a = start_a..(start_a + n);
+
+        let mut a_mut = a;
+
+        set_bits_from_slice_via::<_, _, V>(&mut a_mut, range_a.clone(), &b, start_b);
+
+        let i: usize = kani::any();
+        kani::assume(i < a.len() * T::NUM_BITS);
+
+        let val = get_bit(&a_mut, i);
+
+        let val_expected = if range_a.contains(&i) {
+            get_bit(&b, i - start_a + start_b)
+        } else {
+            get_bit(&a, i)
+        };
+
+        assert_eq!(val, val_expected);
+    }
+}

hacking/kani/.gitignore

@@ -0,0 +1 @@
+/target/

hacking/kani/Makefile

@@ -0,0 +1,14 @@
+BUILD ?= .
+
+build_dir := $(BUILD)
+target_dir := $(build_dir)/target
+
+crates := \
+	sel4-bitfield-ops
+
+.PHONY: none
+none:
+
+.PHONY: check
+check:
+	cargo kani --target-dir=$(abspath $(target_dir)) $(addprefix -p,$(crates))

hacking/kani/docker/Dockerfile

@@ -0,0 +1,34 @@
+FROM debian:bookworm
+
+RUN apt-get update -q && apt-get install -y --no-install-recommends \
+    bash-completion \
+    build-essential \
+    ca-certificates \
+    curl \
+    make \
+    man \
+    procps \
+    python3-pip \
+    sudo \
+    vim \
+    && rm -rf /var/lib/apt/lists/*
+
+ARG UID
+ARG GID
+
+RUN groupadd -f -g $GID x && useradd -u $UID -g $GID -G sudo -m -p x x
+RUN echo '%sudo ALL=(ALL) NOPASSWD:ALL' >> /etc/sudoers # for convenience
+
+USER x
+
+# Optimize by matching rust-toolchain.toml
+ENV DEFAULT_TOOLCHAIN=nightly-2023-08-02
+
+RUN curl -sSf https://sh.rustup.rs | \
+        bash -s -- -y --no-modify-path --default-toolchain $DEFAULT_TOOLCHAIN
+
+ENV PATH=/home/x/.cargo/bin:$PATH
+
+RUN cargo install --locked kani-verifier && cargo kani setup
+
+WORKDIR /work

hacking/kani/docker/Makefile

@@ -0,0 +1,49 @@
+work_root := ../../..
+here_relative := hacking/kani
+
+id := rust-sel4-kani
+image_tag := $(id)
+container_name := $(id)
+
+uid := $(shell id -u)
+gid := $(shell id -g)
+
+mount_params := type=bind,src=$(abspath $(work_root)),dst=/work
+
+.PHONY: none
+none:
+
+.PHONY: build
+build:
+	docker build \
+		--build-arg UID=$(uid) --build-arg GID=$(gid) \
+		-t $(image_tag) .
+
+.PHONY: run
+run: build
+	docker run -d --name $(container_name) \
+		--mount $(mount_params) \
+		$(image_tag) sleep inf
+
+.PHONY: runi
+runi: build
+	docker run --rm \
+		--mount $(mount_params) \
+		-it $(image_tag) bash
+
+.PHONY: exec
+exec:
+	docker exec -it $(container_name) bash
+
+.PHONY: rm-container
+rm-container:
+	for id in $$(docker ps -aq -f "name=^$(container_name)$$"); do \
+		docker rm -f $$id; \
+	done
+
+.PHONY: check
+check: build
+	docker run --rm \
+		--mount $(mount_params),readonly \
+		-i $(image_tag) \
+		make -C $(here_relative) check BUILD=/tmp/build