Bump Rust + RefinedRust versions (#112)

* bump RefinedRust + Rust
* update readme

---------

Signed-off-by: Lennard Gäher <[email protected]>

Author: lgaeher

.github/workflows/verify.yml

@@ -22,8 +22,6 @@ jobs:
       run: opam init -y
     - name: Setup opam switch
       run: opam switch create refinedrust-ace --packages=ocaml-variants.4.14.1+options,ocaml-option-flambda
-    - name: Install coq
-      run: eval $(opam env) && opam update && opam pin add coq 8.17.1 -y
     - name: ls
       run: ls -la .
     - name: Install openssl dependency
@@ -44,8 +42,6 @@ jobs:
       run: cargo --version 
     - name: Install RefinedRust stdlib
       run: eval $(opam env) && REFINEDRUST_ROOT=$PWD/verification/refinedrust ./verification/refinedrust/scripts/install-stdlib.sh
-    - name: Generate stdlib metadata
-      run: eval $(opam env) && make -C verification/refinedrust/stdlib generate_stdlib
     - name: Exclude RefinedRust from dune build
       run: echo "(dirs :standard \ generated_code.bak refinedrust)" > verification/dune
     - name: install build dependencies
@@ -59,4 +55,4 @@ jobs:
     - name: make devtools
       run: source "$HOME/.cargo/env" && eval $(opam env) && make devtools
     - name: Translate specified files using RefinedRust and check proofs
-      run: source "$HOME/.cargo/env" && eval $(opam env) && make verify
+      run: source "$HOME/.cargo/env" && eval $(opam env) && DUNEFLAGS="-j 1" make verify

.gitignore

@@ -3,10 +3,9 @@
 /target/
 build/*
 target/*
+**/target
 
-tools/cove_tap_tool/target
 qemu/
-security-monitor/target
 
 configurations/overlay/root/harness/baremetal
 confidential-vms/linux_vm/configurations/package_override.dev
@@ -23,4 +22,4 @@ Cargo.lock
 *.ko
 
 # skip log files
-*.log
+*.log

Makefile

@@ -26,7 +26,7 @@ export LINUX_IMAGE						?= $(HYPERVISOR_WORK_DIR)/buildroot/images/Image
 export TOOLS_SOURCE_DIR					?= $(MAKEFILE_SOURCE_DIR)/tools
 export TOOLS_WORK_DIR					?= $(ACE_DIR)/tools
 
-export CROSS_COMPILE					= riscv64-unknown-linux-gnu-
+export CROSS_COMPILE					?= riscv64-unknown-linux-gnu-
 export PLATFORM_RISCV_XLEN				= 64
 export PLATFORM_RISCV_ISA				= rv64gc
 export PLATFORM_RISCV_ABI				= lp64d

rust-toolchain.toml

@@ -1,3 +1,3 @@
 [toolchain]
-channel = "nightly-2023-09-15"
-targets = [ "riscv64gc-unknown-none-elf" ]
+channel = "nightly-2025-09-12"
+targets = [ "riscv64gc-unknown-none-elf" ]

security-monitor/Makefile

@@ -38,7 +38,7 @@ build: opensbi_bindings fmt
 refinedrust: opensbi_bindings
 	echo "Generating RefinedRust translation" ;\
 	mkdir -p $(SM_WORK_DIR) ; \
-	RUSTFLAGS='$(RUSTFLAGS)' CARGO_TARGET_DIR=$(SM_WORK_DIR) INSTALL_DIR=$(ACE_DIR) $(CARGO) refinedrust $(RELEASE) $(TARGET) --features verbose ; \
+	RUSTFLAGS='$(RUSTFLAGS)' CARGO_TARGET_DIR=$(SM_WORK_DIR) INSTALL_DIR=$(ACE_DIR) $(CARGO) refinedrust -- $(RELEASE) $(TARGET) --features verbose; \
 	rm -rf $(OPENSBI_WORK_DIR)/
 
 debug: opensbi_bindings

security-monitor/rust-crates/pointers_utility/src/lib.rs

@@ -3,22 +3,25 @@
 // SPDX-License-Identifier: Apache-2.0
 #![no_std]
 #![no_main]
-#![feature(pointer_byte_offsets)]
 
 // used for RefinedRust annotations
 #![feature(register_tool)]
 #![register_tool(rr)]
 #![feature(custom_inner_attributes)]
 #![rr::coq_prefix("ace_ptr")]
+#![rr::include("stdlib")]
 
 
 mod error;
 use core::mem::size_of;
 pub use crate::error::PointerError;
 
 /// Calculates the offset in bytes between two pointers. 
+#[rr::only_spec]
+#[rr::returns("wrap_to_it (pointer1.2 - pointer2.2) isize")]
 pub fn ptr_byte_offset(pointer1: *const usize, pointer2: *const usize) -> isize {
-    (pointer1 as isize) - (pointer2 as isize)
+    // TODO: we should use wrapping arithmetic here, as it might overflow
+    (pointer1.addr() as isize) - (pointer2.addr() as isize)
 }
 
 /// Aligns the pointer to specific size while making sure that the aligned pointer
@@ -34,11 +37,9 @@ pub fn ptr_align(pointer: *mut usize, align_in_bytes: usize, owned_region_end: *
 /// the one-past-the-end address. The returned pointer is guaranteed to be valid for accesses
 /// of size one, if the original pointer is valid. Additional checks are required for making
 /// larger memory accesses.
-#[rr::skip]
-#[rr::params("l", "off", "lmax")]
-#[rr::args("l", "off", "lmax")]
-#[rr::requires("⌜l.2 + off < lmax.2⌝")]
-#[rr::returns("Ok(l +ₗ off)")]
+#[rr::ok]
+#[rr::requires("pointer.2 + offset_in_bytes < owned_region_end.2")]
+#[rr::ensures("ret = (pointer +ₗ offset_in_bytes)")]
 pub fn ptr_byte_add_mut(
     pointer: *mut usize, offset_in_bytes: usize, owned_region_end: *const usize,
 ) -> Result<*mut usize, PointerError> {
@@ -59,6 +60,9 @@ pub fn ptr_byte_add_mut(
 /// the one-past-the-end address. The returned pointer is guaranteed to be valid for accesses
 /// of size one, if the original pointer is valid. Additional checks are required for making
 /// larger memory accesses.
+#[rr::ok]
+#[rr::requires("pointer.2 + offset_in_bytes < owned_region_end.2")]
+#[rr::ensures("ret = (pointer +ₗ offset_in_bytes)")]
 pub fn ptr_byte_add(
     pointer: *const usize, offset_in_bytes: usize, owned_region_end: *const usize,
 ) -> Result<*const usize, PointerError> {

security-monitor/src/confidential_flow/finite_state_machine.rs

@@ -315,23 +315,23 @@ impl<'a> ConfidentialFlow<'a> {
         self
     }
 
-    pub fn confidential_vm_id(&'a self) -> ConfidentialVmId {
+    pub fn confidential_vm_id(&self) -> ConfidentialVmId {
         self.confidential_hart().confidential_vm_id().expect(Self::DUMMY_HART_ERROR_MSG)
     }
 
-    fn confidential_hart_id(&'a self) -> usize {
+    fn confidential_hart_id(&self) -> usize {
         self.confidential_hart().confidential_hart_id()
     }
 
     fn confidential_hart_mut(&mut self) -> &mut ConfidentialHart {
         self.hardware_hart.confidential_hart_mut()
     }
 
-    fn confidential_hart(&'a self) -> &ConfidentialHart {
+    fn confidential_hart(&self) -> &ConfidentialHart {
         self.hardware_hart.confidential_hart()
     }
 
-    fn hypervisor_hart(&'a self) -> &HypervisorHart {
+    fn hypervisor_hart(&self) -> &HypervisorHart {
         &self.hardware_hart.hypervisor_hart()
     }
 }

security-monitor/src/core/architecture/riscv/mmu/page_size.rs

@@ -2,7 +2,6 @@
 // SPDX-FileContributor: Wojciech Ozga <[email protected]>, IBM Research - Zurich
 // SPDX-License-Identifier: Apache-2.0
 #![rr::import("ace.theories.page_allocator", "page")]
-#![rr::include("option")]
 
 // The order of page size in this enum must follow the increasing sizes of page to guarantee that the Ord/PartialOrd are correctly derived
 // for the `PageSize`.
@@ -30,10 +29,9 @@ impl PageSize {
     // and 4KiB).
     pub const TYPICAL_NUMBER_OF_PAGES_INSIDE_LARGER_PAGE: usize = 512;
 
+    // TODO: need performance optimizations for verifying this
     #[rr::trust_me]
-    #[rr::params("x")]
-    #[rr::args("#x")]
-    #[rr::returns("page_size_in_bytes_Z x")]
+    #[rr::returns("page_size_in_bytes_Z self")]
     pub fn in_bytes(&self) -> usize {
         match self {
             PageSize::Size128TiB => 8 * 512 * 512 * 512 * 512 * 256,
@@ -45,10 +43,7 @@ impl PageSize {
         }
     }
 
-    #[rr::trust_me]
-    #[rr::params("x")]
-    #[rr::args("#x")]
-    #[rr::returns("<#>@{option} page_size_smaller x")]
+    #[rr::returns("page_size_smaller self")]
     pub fn smaller(&self) -> Option<PageSize> {
         match self {
             PageSize::Size128TiB => Some(PageSize::Size512GiB),
@@ -60,10 +55,7 @@ impl PageSize {
         }
     }
 
-    #[rr::trust_me]
-    #[rr::params("x")]
-    #[rr::args("#x")]
-    #[rr::returns("<#>@{option} page_size_larger x")]
+    #[rr::returns("page_size_larger self")]
     pub fn larger(&self) -> Option<PageSize> {
         match self {
             PageSize::Size128TiB => None,
@@ -75,10 +67,7 @@ impl PageSize {
         }
     }
 
-    #[rr::trust_me]
-    #[rr::params("x")]
-    #[rr::args("#x")]
-    #[rr::returns("page_size_multiplier x")]
+    #[rr::returns("number_of_smaller_pages self")]
     pub fn number_of_smaller_pages(&self) -> usize {
         match self {
             PageSize::Size128TiB => 256,

security-monitor/src/core/architecture/riscv/mmu/page_table_level.rs

@@ -20,10 +20,7 @@ pub enum PageTableLevel {
 }
 
 impl PageTableLevel {
-    #[rr::trust_me]
-    #[rr::params("x")]
-    #[rr::args("#x")]
-    #[rr::returns("<#>@{option} (page_table_level_lower x)")]
+    #[rr::returns("page_table_level_lower self")]
     pub fn lower(&self) -> Option<Self> {
         match self {
             Self::Level5 => Some(Self::Level4),

security-monitor/src/core/architecture/riscv/mmu/paging_system.rs

@@ -11,8 +11,9 @@ use crate::core::memory_layout::ConfidentialVmPhysicalAddress;
 #[derive(Debug, Copy, Clone)]
 #[rr::refined_by("paging_system")]
 pub enum PagingSystem {
+    #[rr::pattern("Sv48")]
     Sv48x4,
-    #[rr::pattern("Sv57x4")]
+    #[rr::pattern("Sv57")]
     Sv57x4,
 }
 
@@ -31,10 +32,7 @@ impl PagingSystem {
         }
     }
 
-    #[rr::skip]
-    #[rr::params("system")]
-    #[rr::args("#system")]
-    #[rr::returns("paging_system_highest_level system")]
+    #[rr::returns("paging_system_highest_level self")]
     pub fn levels(&self) -> PageTableLevel {
         match self {
             PagingSystem::Sv48x4 => PageTableLevel::Level4,