Function Contracts: Interior Mutability Tests

rfc/src/rfcs/0009-function-contracts.md

@@ -706,6 +706,22 @@ structures however are ubiquitous and users can avoid the unsoundness with
 relative confidence by overprovisioning (generating inputs that are several
 times larger than what they expect the function will touch).
 
+### Interior Mutability
+
+In Rust, if a struct is immutable, all fields within it are immutable. However, we can still mutate some of these fields via an interface that allows us to do so: https://doc.rust-lang.org/std/cell/.
+
+In Goto, there is no distinction between immutable and mutable fields, thus breaking this encapsulation that Rust provides. We can leverage this encapsulation breaking mechanic to write verified proofs of Rust interior mutability, as long as we preserve the overall properties that the encapsulation would have given us.
+
+It is possible to represent the abstraction breaking mechanics within unsafe Rust for `UnsafeCell` and `Cell` as explained by the memory layout properies ensured during compilation: https://doc.rust-lang.org/std/cell/struct.UnsafeCell.html#memory-layout. While we cannot access private fields in Rust, we can interpret the fields as an arbitrary pointer to the type of the field via a transmute if we know the data layout of the field. It is thus possible to safely verify code for `UnsafeCell` and `Cell` within Kani by breaking the encapsulation with unsafe rust.
+
+`OnceCell` follows the pattern of having only one field within the struct, thus access to this struct via an unsafe transmute is predictable within the Kani compiler, although this behavior is not explicitly explained in Rust documentation as it is for `UnsafeCell` and `Cell`. We can verify code for `OnceCell` within Kani, but we need to be more careful in assessing whether this is UB or not.
+
+This is much harder for `RefCell` as it is UB to rely on the particular order of fields in a struct, and there might be inconsistent padding through compilation. It should be possible to attach a compilation tool within Kani to expose these private fields after they have been compiled to Goto, but this still creates risk that these private fields could be modified or accessed in a way that is UB to do so from the Rust standpoint.
+
+We focus on single threaded computation, so we avoid verifying `RwLock`, `Mutex` and similar other constructs for now.
+
+It is important to further investigate this discrepency between encapulsation at the Rust level and Goto level. When is it safe to break encapsulation and how should we break encapsulation in a way that preserves encapsulation properties? Can we represent and verify Rust encapsulation properties at the Goto level? Is there a modification to the `modifies` and `assigns` function contracts that would allow us to demonstrate these encapsulation properties? These questions are all important if we wish to perserve full abstraction correctness in the compilation between Rust and Goto.
+
 
 ## Open questions
 

tests/expected/function-contract/interior-mutability/api/cell.expected

@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| im.x.get() < 101"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/interior-mutability/api/cell.rs

@@ -0,0 +1,27 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+/// Mutating Cell via as_ptr in contracts
+use std::cell::Cell;
+
+/// This struct is contains Cell which can be mutated
+struct InteriorMutability {
+ x: Cell<u32>,
+}
+
+/// contracts need to access im.x internal data through the api im.x.as_ptr
+#[kani::requires(im.x.get() < 100)]
+#[kani::modifies(im.x.as_ptr())]
+#[kani::ensures(|_| im.x.get() < 101)]
+///im is an immutable reference with interior mutability
+fn modify(im: &InteriorMutability) {
+ /// valid rust methodology for getting and setting value without breaking encapsulation
+ im.x.set(im.x.get() + 1)
+}
+
+#[kani::proof_for_contract(modify)]
+fn harness_for_modify() {
+ let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) };
+ modify(&im)
+}

tests/expected/function-contract/interior-mutability/api/unsafecell.expected

@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| unsafe{ *im.x.get() } < 101"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/interior-mutability/api/unsafecell.rs

@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+use std::cell::UnsafeCell;
+
+/// This struct is contains UnsafeCell which can be mutated
+struct InteriorMutability {
+ x: UnsafeCell<u32>,
+}
+
+/// contracts need to access im.x internal data through im.x.get() with an unsafe raw pointer dereference
+#[kani::requires(unsafe{*im.x.get()} < 100)]
+#[kani::modifies(im.x.get())]
+#[kani::ensures(|_| unsafe{*im.x.get()} < 101)]
+///im is an immutable reference with interior mutability
+fn modify(im: &InteriorMutability) {
+ unsafe { *im.x.get() += 1 }
+}
+
+#[kani::proof_for_contract(modify)]
+fn harness_for_modify() {
+ let im: InteriorMutability = InteriorMutability { x: UnsafeCell::new(kani::any()) };
+ modify(&im)
+}

tests/expected/function-contract/interior-mutability/transmute/cell.expected

@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| *unsafe{ im.x.expose() } < 101"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/interior-mutability/transmute/cell.rs

@@ -0,0 +1,48 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+/// The objective of this test is to check the modification of a Cell used as interior mutability in an immutable struct
+
+/// ---------------------------------------------------
+/// Abstraction Breaking Functionality
+/// ---------------------------------------------------
+use std::cell::Cell;
+use std::mem::transmute;
+
+/// This exposes the underlying representation so that it can be added into a modifies clause within kani
+trait Exposeable<T: ?Sized> {
+ unsafe fn expose(&self) -> &T;
+}
+
+/// This unsafe manipulation is valid due to Cell having the same underlying data layout as its internal T as explained here: https://doc.rust-lang.org/stable/std/cell/struct.Cell.html#memory-layout
+impl<T: ?Sized> Exposeable<T> for Cell<T> {
+ unsafe fn expose(&self) -> &T {
+ transmute(self)
+ }
+}
+
+/// ---------------------------------------------------
+/// Test Case
+/// ---------------------------------------------------
+
+/// This struct is contains Cell which can be mutated
+struct InteriorMutability {
+ x: Cell<u32>,
+}
+
+/// contracts need to access im.x internal data through the unsafe function im.x.expose()
+#[kani::requires(*unsafe{im.x.expose()} < 100)]
+#[kani::modifies(im.x.expose())]
+#[kani::ensures(|_| *unsafe{im.x.expose()} < 101)]
+///im is an immutable reference with interior mutability
+fn modify(im: &InteriorMutability) {
+ /// valid rust methodology for getting and setting value without breaking encapsulation
+ im.x.set(im.x.get() + 1)
+}
+
+#[kani::proof_for_contract(modify)]
+fn harness_for_modify() {
+ let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) };
+ modify(&im)
+}

tests/expected/function-contract/interior-mutability/transmute/cell_stub.expected

@@ -0,0 +1,13 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| old(*unsafe{ im.x.expose() } + *unsafe{ im.x.expose() }) ==\
+*unsafe{ im.x.expose() }"\
+
+assertion\
+- Status: SUCCESS\
+- Description: "|_|
+old(*unsafe{ im.x.expose() } + *unsafe{ im.x.expose() } +\
+*unsafe{ im.x.expose() } + *unsafe{ im.x.expose() }) ==\
+*unsafe{ im.x.expose() }"\
+
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/interior-mutability/transmute/cell_stub.rs

@@ -0,0 +1,61 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+/// The objective of this test is to show that the contracts for double can be replaced as a stub within the contracts for quadruple.
+/// This shows that we can generate kani::any() for Cell safely by breaking encapsulation
+
+/// ---------------------------------------------------
+/// Abstraction Breaking Functionality
+/// ---------------------------------------------------
+use std::cell::Cell;
+use std::mem::transmute;
+
+/// This exposes the underlying representation so that it can be added into a modifies clause within kani
+trait Exposeable<T: ?Sized> {
+ unsafe fn expose(&self) -> &T;
+}
+
+/// This unsafe manipulation is valid due to Cell having the same underlying data layout as its internal T as explained here: https://doc.rust-lang.org/stable/std/cell/struct.Cell.html#memory-layout
+impl<T: ?Sized> Exposeable<T> for Cell<T> {
+ unsafe fn expose(&self) -> &T {
+ transmute(self)
+ }
+}
+
+/// ---------------------------------------------------
+/// Test Case
+/// ---------------------------------------------------
+
+/// This struct is contains Cell which can be mutated
+struct InteriorMutability {
+ x: Cell<u32>,
+}
+
+#[kani::ensures(|_| old(*unsafe{im.x.expose()} + *unsafe{im.x.expose()}) == *unsafe{im.x.expose()})]
+#[kani::requires(*unsafe{im.x.expose()} < 100)]
+#[kani::modifies(im.x.expose())]
+fn double(im: &InteriorMutability) {
+ im.x.set(im.x.get() + im.x.get())
+}
+
+#[kani::proof_for_contract(double)]
+fn double_harness() {
+ let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) };
+ double(&im);
+}
+
+#[kani::ensures(|_| old(*unsafe{im.x.expose()} + *unsafe{im.x.expose()} + *unsafe{im.x.expose()} + *unsafe{im.x.expose()}) == *unsafe{im.x.expose()})]
+#[kani::requires(*unsafe{im.x.expose()} < 50)]
+#[kani::modifies(im.x.expose())]
+fn quadruple(im: &InteriorMutability) {
+ double(im);
+ double(im)
+}
+
+#[kani::proof_for_contract(quadruple)]
+#[kani::stub_verified(double)]
+fn quadruple_harness() {
+ let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) };
+ quadruple(&im);
+}

tests/expected/function-contract/interior-mutability/transmute/oncecell.expected

@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| unsafe{ im.x.expose() }.is_some()"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/interior-mutability/transmute/oncecell.rs

@@ -0,0 +1,47 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+/// The objective of this test is to check the modification of an OnceCell used as interior mutability in an immutable struct
+
+/// ---------------------------------------------------
+/// Abstraction Breaking Functionality
+/// ---------------------------------------------------
+use std::cell::OnceCell;
+use std::mem::transmute;
+
+/// This exposes the underlying representation so that it can be added into a modifies clause within kani
+trait Exposeable<T: ?Sized> {
+ unsafe fn expose(&self) -> &T;
+}
+
+/// While this is not explicitly labeled as safe in the Rust documentation, it works due to OnceCell having a single field in its struct definition
+impl<T> Exposeable<Option<T>> for OnceCell<T> {
+ unsafe fn expose(&self) -> &Option<T> {
+ transmute(self)
+ }
+}
+
+/// ---------------------------------------------------
+/// Test Case
+/// ---------------------------------------------------
+
+/// This struct is contains OnceCell which can be mutated
+struct InteriorMutability {
+ x: OnceCell<u32>,
+}
+
+/// contracts need to access im.x internal data through the unsafe function im.x.expose()
+#[kani::requires(unsafe{im.x.expose()}.is_none())]
+#[kani::modifies(im.x.expose())]
+#[kani::ensures(|_| unsafe{im.x.expose()}.is_some())]
+fn modify(im: &InteriorMutability) {
+ /// method for setting value in OnceCell without breaking encapsulation
+ im.x.set(5).expect("")
+}
+
+#[kani::proof_for_contract(modify)]
+fn harness_for_modify() {
+ let im: InteriorMutability = InteriorMutability { x: OnceCell::new() };
+ modify(&im)
+}

tests/expected/function-contract/interior-mutability/transmute/unsafecell.expected

@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| *unsafe{ im.x.expose() } < 101"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/interior-mutability/transmute/unsafecell.rs

@@ -0,0 +1,47 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+/// The objective of this test is to check the modification of an UnsafeCell used as interior mutability in an immutable struct
+
+/// ---------------------------------------------------
+/// Abstraction Breaking Functionality
+/// ---------------------------------------------------
+use std::cell::UnsafeCell;
+use std::mem::transmute;
+
+/// This exposes the underlying representation so that it can be added into a modifies clause within kani
+trait Exposeable<T: ?Sized> {
+ unsafe fn expose(&self) -> &T;
+}
+
+/// This unsafe manipulation is valid due to UnsafeCell having the same underlying data layout as its internal T as explained here: https://doc.rust-lang.org/stable/std/cell/struct.UnsafeCell.html#memory-layout
+impl<T: ?Sized> Exposeable<T> for UnsafeCell<T> {
+ unsafe fn expose(&self) -> &T {
+ transmute(self)
+ }
+}
+
+/// ---------------------------------------------------
+/// Test Case
+/// ---------------------------------------------------
+
+/// This struct is contains UnsafeCell which can be mutated
+struct InteriorMutability {
+ x: UnsafeCell<u32>,
+}
+
+/// contracts need to access im.x internal data through the unsafe function im.x.expose()
+#[kani::requires(*unsafe{im.x.expose()} < 100)]
+#[kani::modifies(im.x.expose())]
+#[kani::ensures(|_| *unsafe{im.x.expose()} < 101)]
+///im is an immutable reference with interior mutability
+fn modify(im: &InteriorMutability) {
+ unsafe { *im.x.get() += 1 }
+}
+
+#[kani::proof_for_contract(modify)]
+fn harness_for_modify() {
+ let im: InteriorMutability = InteriorMutability { x: UnsafeCell::new(kani::any()) };
+ modify(&im)
+}