From ed8fee11bccbb0bf9f6a1a19f73d3300dd6bbda2 Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Wed, 17 Jul 2024 17:35:49 -0400
Subject: [PATCH 01/32] add tests

---
 .../interior-mutability/cell.expected         |  6 ++
 .../interior-mutability/cell.rs               | 61 +++++++++++++++++++
 .../interior-mutability/unsafecell.expected   |  6 ++
 .../interior-mutability/unsafecell.rs         | 61 +++++++++++++++++++
 4 files changed, 134 insertions(+)
 create mode 100644 tests/expected/function-contract/interior-mutability/cell.expected
 create mode 100644 tests/expected/function-contract/interior-mutability/cell.rs
 create mode 100644 tests/expected/function-contract/interior-mutability/unsafecell.expected
 create mode 100644 tests/expected/function-contract/interior-mutability/unsafecell.rs

diff --git a/tests/expected/function-contract/interior-mutability/cell.expected b/tests/expected/function-contract/interior-mutability/cell.expected
new file mode 100644
index 000000000000..f98d1759dbab
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/cell.expected
@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| unsafe{x.x.hack()}.value.value < 101"\
+in function max
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/cell.rs b/tests/expected/function-contract/interior-mutability/cell.rs
new file mode 100644
index 000000000000..8f07344a555f
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/cell.rs
@@ -0,0 +1,61 @@
+use std::cell::{Cell, RefCell, UnsafeCell};
+use std::mem::transmute;
+use std::panic;
+
+#[allow(dead_code)]
+pub struct UnsafeCellHack<T: ?Sized> {
+    value: T,
+}
+
+#[allow(dead_code)]
+pub struct CellHack<T: ?Sized> {
+    value: UnsafeCellHack<T>,
+}
+
+#[allow(dead_code)]
+pub struct RefCellHack<T: ?Sized> {
+    borrow: CellHack<isize>,
+    borrowed_at: CellHack<Option<&'static crate::panic::Location<'static>>>,
+    value: UnsafeCellHack<T>,
+}
+
+trait ToHack<T> {
+    unsafe fn hack(&self) -> &T;
+}
+
+impl<T> ToHack<UnsafeCellHack<T>> for UnsafeCell<T> {
+    unsafe fn hack(&self) -> &UnsafeCellHack<T> {
+        transmute(self)
+    }
+}
+
+impl<T> ToHack<CellHack<T>> for Cell<T> {
+    unsafe fn hack(&self) -> &CellHack<T> {
+        transmute(self)
+    }
+}
+
+impl<T> ToHack<RefCellHack<T>> for RefCell<T> {
+    unsafe fn hack(&self) -> &RefCellHack<T> {
+        transmute(self)
+    }
+}
+
+// ---------------------------------------------------
+
+struct InteriorMutability {
+    x: Cell<u32>,
+}
+
+#[kani::requires(unsafe{x.x.hack()}.value.value < 100)]
+#[kani::modifies(&x.x.hack().value.value)]
+#[kani::ensures(|_| unsafe{x.x.hack()}.value.value < 101)]
+fn modify(x: &InteriorMutability) {
+    x.x.set(x.x.get() + 1)
+}
+
+#[kani::proof_for_contract(modify)]
+fn main() {
+    let x: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) };
+    modify(&x)
+}
diff --git a/tests/expected/function-contract/interior-mutability/unsafecell.expected b/tests/expected/function-contract/interior-mutability/unsafecell.expected
new file mode 100644
index 000000000000..15a4dd00b4b3
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/unsafecell.expected
@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| unsafe{x.x.hack()}.value < 101"\
+in function max
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/unsafecell.rs b/tests/expected/function-contract/interior-mutability/unsafecell.rs
new file mode 100644
index 000000000000..3ecf3df831e2
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/unsafecell.rs
@@ -0,0 +1,61 @@
+use std::cell::{Cell, RefCell, UnsafeCell};
+use std::mem::transmute;
+use std::panic;
+
+#[allow(dead_code)]
+pub struct UnsafeCellHack<T: ?Sized> {
+    value: T,
+}
+
+#[allow(dead_code)]
+pub struct CellHack<T: ?Sized> {
+    value: UnsafeCellHack<T>,
+}
+
+#[allow(dead_code)]
+pub struct RefCellHack<T: ?Sized> {
+    borrow: CellHack<isize>,
+    borrowed_at: CellHack<Option<&'static crate::panic::Location<'static>>>,
+    value: UnsafeCellHack<T>,
+}
+
+trait ToHack<T> {
+    unsafe fn hack(&self) -> &T;
+}
+
+impl<T> ToHack<UnsafeCellHack<T>> for UnsafeCell<T> {
+    unsafe fn hack(&self) -> &UnsafeCellHack<T> {
+        transmute(self)
+    }
+}
+
+impl<T> ToHack<CellHack<T>> for Cell<T> {
+    unsafe fn hack(&self) -> &CellHack<T> {
+        transmute(self)
+    }
+}
+
+impl<T> ToHack<RefCellHack<T>> for RefCell<T> {
+    unsafe fn hack(&self) -> &RefCellHack<T> {
+        transmute(self)
+    }
+}
+
+// ---------------------------------------------------
+
+struct InteriorMutability {
+    x: UnsafeCell<u32>,
+}
+
+#[kani::requires(unsafe{x.x.hack()}.value < 100)]
+#[kani::modifies(&x.x.hack().value)]
+#[kani::ensures(|_| unsafe{x.x.hack()}.value < 101)]
+fn modify(x: &InteriorMutability) {
+    unsafe { *x.x.get() += 1 }
+}
+
+#[kani::proof_for_contract(modify)]
+fn main() {
+    let x: InteriorMutability = InteriorMutability { x: UnsafeCell::new(kani::any()) };
+    modify(&x)
+}

From 0bbd78b4cd6e4a194b4a567699b31ee278253f19 Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Wed, 17 Jul 2024 17:49:53 -0400
Subject: [PATCH 02/32] fix tests

---
 .../function-contract/interior-mutability/cell.expected       | 4 ++--
 tests/expected/function-contract/interior-mutability/cell.rs  | 4 ++++
 .../function-contract/interior-mutability/unsafecell.expected | 4 ++--
 .../function-contract/interior-mutability/unsafecell.rs       | 4 ++++
 4 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/tests/expected/function-contract/interior-mutability/cell.expected b/tests/expected/function-contract/interior-mutability/cell.expected
index f98d1759dbab..2d8e52a4d07b 100644
--- a/tests/expected/function-contract/interior-mutability/cell.expected
+++ b/tests/expected/function-contract/interior-mutability/cell.expected
@@ -1,6 +1,6 @@
 assertion\
 - Status: SUCCESS\
-- Description: "|_| unsafe{x.x.hack()}.value.value < 101"\
-in function max
+- Description: "|_| unsafe{ x.x.hack() }.value.value < 101"\
+in function modify
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/cell.rs b/tests/expected/function-contract/interior-mutability/cell.rs
index 8f07344a555f..c8a939373198 100644
--- a/tests/expected/function-contract/interior-mutability/cell.rs
+++ b/tests/expected/function-contract/interior-mutability/cell.rs
@@ -1,3 +1,7 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
 use std::cell::{Cell, RefCell, UnsafeCell};
 use std::mem::transmute;
 use std::panic;
diff --git a/tests/expected/function-contract/interior-mutability/unsafecell.expected b/tests/expected/function-contract/interior-mutability/unsafecell.expected
index 15a4dd00b4b3..1cefb92b2c5d 100644
--- a/tests/expected/function-contract/interior-mutability/unsafecell.expected
+++ b/tests/expected/function-contract/interior-mutability/unsafecell.expected
@@ -1,6 +1,6 @@
 assertion\
 - Status: SUCCESS\
-- Description: "|_| unsafe{x.x.hack()}.value < 101"\
-in function max
+- Description: "|_| unsafe{ x.x.hack() }.value < 101"\
+in function modify
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/unsafecell.rs b/tests/expected/function-contract/interior-mutability/unsafecell.rs
index 3ecf3df831e2..4202a864f7b1 100644
--- a/tests/expected/function-contract/interior-mutability/unsafecell.rs
+++ b/tests/expected/function-contract/interior-mutability/unsafecell.rs
@@ -1,3 +1,7 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
 use std::cell::{Cell, RefCell, UnsafeCell};
 use std::mem::transmute;
 use std::panic;

From 35a9320307758919849122ca006046bbd41359d7 Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Wed, 17 Jul 2024 19:27:50 -0400
Subject: [PATCH 03/32] preserves memory

---
 .../interior-mutability/cell.expected         |  2 +-
 .../interior-mutability/cell.rs               | 42 ++++---------------
 .../interior-mutability/unsafecell.expected   |  2 +-
 .../interior-mutability/unsafecell.rs         | 42 ++++---------------
 4 files changed, 20 insertions(+), 68 deletions(-)

diff --git a/tests/expected/function-contract/interior-mutability/cell.expected b/tests/expected/function-contract/interior-mutability/cell.expected
index 2d8e52a4d07b..c04e2c96c0c2 100644
--- a/tests/expected/function-contract/interior-mutability/cell.expected
+++ b/tests/expected/function-contract/interior-mutability/cell.expected
@@ -1,6 +1,6 @@
 assertion\
 - Status: SUCCESS\
-- Description: "|_| unsafe{ x.x.hack() }.value.value < 101"\
+- Description: "|_| *unsafe{ x.x.hack() } < 101"\
 in function modify
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/cell.rs b/tests/expected/function-contract/interior-mutability/cell.rs
index c8a939373198..87e8c39b8dfc 100644
--- a/tests/expected/function-contract/interior-mutability/cell.rs
+++ b/tests/expected/function-contract/interior-mutability/cell.rs
@@ -2,45 +2,21 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-use std::cell::{Cell, RefCell, UnsafeCell};
+use std::cell::{Cell, UnsafeCell};
 use std::mem::transmute;
-use std::panic;
 
-#[allow(dead_code)]
-pub struct UnsafeCellHack<T: ?Sized> {
-    value: T,
-}
-
-#[allow(dead_code)]
-pub struct CellHack<T: ?Sized> {
-    value: UnsafeCellHack<T>,
-}
-
-#[allow(dead_code)]
-pub struct RefCellHack<T: ?Sized> {
-    borrow: CellHack<isize>,
-    borrowed_at: CellHack<Option<&'static crate::panic::Location<'static>>>,
-    value: UnsafeCellHack<T>,
-}
-
-trait ToHack<T> {
+trait ToHack<T : ?Sized> {
     unsafe fn hack(&self) -> &T;
 }
 
-impl<T> ToHack<UnsafeCellHack<T>> for UnsafeCell<T> {
-    unsafe fn hack(&self) -> &UnsafeCellHack<T> {
-        transmute(self)
-    }
-}
-
-impl<T> ToHack<CellHack<T>> for Cell<T> {
-    unsafe fn hack(&self) -> &CellHack<T> {
+impl<T : ?Sized> ToHack<T> for UnsafeCell<T> {
+    unsafe fn hack(&self) -> &T {
         transmute(self)
     }
 }
 
-impl<T> ToHack<RefCellHack<T>> for RefCell<T> {
-    unsafe fn hack(&self) -> &RefCellHack<T> {
+impl<T : ?Sized> ToHack<T> for Cell<T> {
+    unsafe fn hack(&self) -> &T {
         transmute(self)
     }
 }
@@ -51,9 +27,9 @@ struct InteriorMutability {
     x: Cell<u32>,
 }
 
-#[kani::requires(unsafe{x.x.hack()}.value.value < 100)]
-#[kani::modifies(&x.x.hack().value.value)]
-#[kani::ensures(|_| unsafe{x.x.hack()}.value.value < 101)]
+#[kani::requires(*unsafe{x.x.hack()} < 100)]
+#[kani::modifies(x.x.hack())]
+#[kani::ensures(|_| *unsafe{x.x.hack()} < 101)]
 fn modify(x: &InteriorMutability) {
     x.x.set(x.x.get() + 1)
 }
diff --git a/tests/expected/function-contract/interior-mutability/unsafecell.expected b/tests/expected/function-contract/interior-mutability/unsafecell.expected
index 1cefb92b2c5d..c04e2c96c0c2 100644
--- a/tests/expected/function-contract/interior-mutability/unsafecell.expected
+++ b/tests/expected/function-contract/interior-mutability/unsafecell.expected
@@ -1,6 +1,6 @@
 assertion\
 - Status: SUCCESS\
-- Description: "|_| unsafe{ x.x.hack() }.value < 101"\
+- Description: "|_| *unsafe{ x.x.hack() } < 101"\
 in function modify
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/unsafecell.rs b/tests/expected/function-contract/interior-mutability/unsafecell.rs
index 4202a864f7b1..c93ceea072b2 100644
--- a/tests/expected/function-contract/interior-mutability/unsafecell.rs
+++ b/tests/expected/function-contract/interior-mutability/unsafecell.rs
@@ -2,45 +2,21 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-use std::cell::{Cell, RefCell, UnsafeCell};
+use std::cell::{Cell, UnsafeCell};
 use std::mem::transmute;
-use std::panic;
 
-#[allow(dead_code)]
-pub struct UnsafeCellHack<T: ?Sized> {
-    value: T,
-}
-
-#[allow(dead_code)]
-pub struct CellHack<T: ?Sized> {
-    value: UnsafeCellHack<T>,
-}
-
-#[allow(dead_code)]
-pub struct RefCellHack<T: ?Sized> {
-    borrow: CellHack<isize>,
-    borrowed_at: CellHack<Option<&'static crate::panic::Location<'static>>>,
-    value: UnsafeCellHack<T>,
-}
-
-trait ToHack<T> {
+trait ToHack<T : ?Sized> {
     unsafe fn hack(&self) -> &T;
 }
 
-impl<T> ToHack<UnsafeCellHack<T>> for UnsafeCell<T> {
-    unsafe fn hack(&self) -> &UnsafeCellHack<T> {
-        transmute(self)
-    }
-}
-
-impl<T> ToHack<CellHack<T>> for Cell<T> {
-    unsafe fn hack(&self) -> &CellHack<T> {
+impl<T : ?Sized> ToHack<T> for UnsafeCell<T> {
+    unsafe fn hack(&self) -> &T {
         transmute(self)
     }
 }
 
-impl<T> ToHack<RefCellHack<T>> for RefCell<T> {
-    unsafe fn hack(&self) -> &RefCellHack<T> {
+impl<T : ?Sized> ToHack<T> for Cell<T> {
+    unsafe fn hack(&self) -> &T {
         transmute(self)
     }
 }
@@ -51,9 +27,9 @@ struct InteriorMutability {
     x: UnsafeCell<u32>,
 }
 
-#[kani::requires(unsafe{x.x.hack()}.value < 100)]
-#[kani::modifies(&x.x.hack().value)]
-#[kani::ensures(|_| unsafe{x.x.hack()}.value < 101)]
+#[kani::requires(*unsafe{x.x.hack()} < 100)]
+#[kani::modifies(x.x.hack())]
+#[kani::ensures(|_| *unsafe{x.x.hack()} < 101)]
 fn modify(x: &InteriorMutability) {
     unsafe { *x.x.get() += 1 }
 }

From 76a9c5485ecb946e635412f8102f3112208c5d2a Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Wed, 17 Jul 2024 19:32:17 -0400
Subject: [PATCH 04/32] fmt

---
 .../expected/function-contract/interior-mutability/cell.rs  | 6 +++---
 .../function-contract/interior-mutability/unsafecell.rs     | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/tests/expected/function-contract/interior-mutability/cell.rs b/tests/expected/function-contract/interior-mutability/cell.rs
index 87e8c39b8dfc..ea162826675f 100644
--- a/tests/expected/function-contract/interior-mutability/cell.rs
+++ b/tests/expected/function-contract/interior-mutability/cell.rs
@@ -5,17 +5,17 @@
 use std::cell::{Cell, UnsafeCell};
 use std::mem::transmute;
 
-trait ToHack<T : ?Sized> {
+trait ToHack<T: ?Sized> {
     unsafe fn hack(&self) -> &T;
 }
 
-impl<T : ?Sized> ToHack<T> for UnsafeCell<T> {
+impl<T: ?Sized> ToHack<T> for UnsafeCell<T> {
     unsafe fn hack(&self) -> &T {
         transmute(self)
     }
 }
 
-impl<T : ?Sized> ToHack<T> for Cell<T> {
+impl<T: ?Sized> ToHack<T> for Cell<T> {
     unsafe fn hack(&self) -> &T {
         transmute(self)
     }
diff --git a/tests/expected/function-contract/interior-mutability/unsafecell.rs b/tests/expected/function-contract/interior-mutability/unsafecell.rs
index c93ceea072b2..a241378ac3c1 100644
--- a/tests/expected/function-contract/interior-mutability/unsafecell.rs
+++ b/tests/expected/function-contract/interior-mutability/unsafecell.rs
@@ -5,17 +5,17 @@
 use std::cell::{Cell, UnsafeCell};
 use std::mem::transmute;
 
-trait ToHack<T : ?Sized> {
+trait ToHack<T: ?Sized> {
     unsafe fn hack(&self) -> &T;
 }
 
-impl<T : ?Sized> ToHack<T> for UnsafeCell<T> {
+impl<T: ?Sized> ToHack<T> for UnsafeCell<T> {
     unsafe fn hack(&self) -> &T {
         transmute(self)
     }
 }
 
-impl<T : ?Sized> ToHack<T> for Cell<T> {
+impl<T: ?Sized> ToHack<T> for Cell<T> {
     unsafe fn hack(&self) -> &T {
         transmute(self)
     }

From 7ca72aaa659873002b3400a713efc8dedc9f31d5 Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Wed, 17 Jul 2024 19:58:11 -0400
Subject: [PATCH 05/32] OnceCell

---
 .../interior-mutability/cell.rs               |  8 +++-
 .../interior-mutability/oncecell.expected     |  6 +++
 .../interior-mutability/oncecell.rs           | 47 +++++++++++++++++++
 .../interior-mutability/unsafecell.rs         |  8 +++-
 4 files changed, 67 insertions(+), 2 deletions(-)
 create mode 100644 tests/expected/function-contract/interior-mutability/oncecell.expected
 create mode 100644 tests/expected/function-contract/interior-mutability/oncecell.rs

diff --git a/tests/expected/function-contract/interior-mutability/cell.rs b/tests/expected/function-contract/interior-mutability/cell.rs
index ea162826675f..7100a26b0670 100644
--- a/tests/expected/function-contract/interior-mutability/cell.rs
+++ b/tests/expected/function-contract/interior-mutability/cell.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-use std::cell::{Cell, UnsafeCell};
+use std::cell::{Cell, OnceCell, UnsafeCell};
 use std::mem::transmute;
 
 trait ToHack<T: ?Sized> {
@@ -21,6 +21,12 @@ impl<T: ?Sized> ToHack<T> for Cell<T> {
     }
 }
 
+impl<T> ToHack<Option<T>> for OnceCell<T> {
+    unsafe fn hack(&self) -> &Option<T> {
+        transmute(self)
+    }
+}
+
 // ---------------------------------------------------
 
 struct InteriorMutability {
diff --git a/tests/expected/function-contract/interior-mutability/oncecell.expected b/tests/expected/function-contract/interior-mutability/oncecell.expected
new file mode 100644
index 000000000000..d6349f472b07
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/oncecell.expected
@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| unsafe{ x.x.hack() }.is_some()"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/oncecell.rs b/tests/expected/function-contract/interior-mutability/oncecell.rs
new file mode 100644
index 000000000000..48e99eea49ad
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/oncecell.rs
@@ -0,0 +1,47 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+use std::cell::{Cell, OnceCell, UnsafeCell};
+use std::mem::transmute;
+
+trait ToHack<T: ?Sized> {
+    unsafe fn hack(&self) -> &T;
+}
+
+impl<T: ?Sized> ToHack<T> for UnsafeCell<T> {
+    unsafe fn hack(&self) -> &T {
+        transmute(self)
+    }
+}
+
+impl<T: ?Sized> ToHack<T> for Cell<T> {
+    unsafe fn hack(&self) -> &T {
+        transmute(self)
+    }
+}
+
+impl<T> ToHack<Option<T>> for OnceCell<T> {
+    unsafe fn hack(&self) -> &Option<T> {
+        transmute(self)
+    }
+}
+
+// ---------------------------------------------------
+
+struct InteriorMutability {
+    x: OnceCell<u32>,
+}
+
+#[kani::requires(unsafe{x.x.hack()}.is_none())]
+#[kani::modifies(x.x.hack())]
+#[kani::ensures(|_| unsafe{x.x.hack()}.is_some())]
+fn modify(x: &InteriorMutability) {
+    x.x.set(5).expect("")
+}
+
+#[kani::proof_for_contract(modify)]
+fn main() {
+    let x: InteriorMutability = InteriorMutability { x: OnceCell::new() };
+    modify(&x)
+}
diff --git a/tests/expected/function-contract/interior-mutability/unsafecell.rs b/tests/expected/function-contract/interior-mutability/unsafecell.rs
index a241378ac3c1..fb17967fbd34 100644
--- a/tests/expected/function-contract/interior-mutability/unsafecell.rs
+++ b/tests/expected/function-contract/interior-mutability/unsafecell.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-use std::cell::{Cell, UnsafeCell};
+use std::cell::{Cell, OnceCell, UnsafeCell};
 use std::mem::transmute;
 
 trait ToHack<T: ?Sized> {
@@ -21,6 +21,12 @@ impl<T: ?Sized> ToHack<T> for Cell<T> {
     }
 }
 
+impl<T> ToHack<Option<T>> for OnceCell<T> {
+    unsafe fn hack(&self) -> &Option<T> {
+        transmute(self)
+    }
+}
+
 // ---------------------------------------------------
 
 struct InteriorMutability {

From 4ce98ad11a9f2c142ff8dd277126c7914822654f Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Thu, 18 Jul 2024 16:31:50 -0400
Subject: [PATCH 06/32] documentation

---
 .../interior-mutability/cell.expected         |  2 +-
 .../interior-mutability/cell.rs               | 50 +++++++++----------
 .../interior-mutability/oncecell.expected     |  2 +-
 .../interior-mutability/oncecell.rs           | 49 +++++++++---------
 .../interior-mutability/unsafecell.expected   |  2 +-
 .../interior-mutability/unsafecell.rs         | 49 +++++++++---------
 6 files changed, 76 insertions(+), 78 deletions(-)

diff --git a/tests/expected/function-contract/interior-mutability/cell.expected b/tests/expected/function-contract/interior-mutability/cell.expected
index c04e2c96c0c2..29d911ad74f4 100644
--- a/tests/expected/function-contract/interior-mutability/cell.expected
+++ b/tests/expected/function-contract/interior-mutability/cell.expected
@@ -1,6 +1,6 @@
 assertion\
 - Status: SUCCESS\
-- Description: "|_| *unsafe{ x.x.hack() } < 101"\
+- Description: "|_| *unsafe{ im.x.expose() } < 101"\
 in function modify
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/cell.rs b/tests/expected/function-contract/interior-mutability/cell.rs
index 7100a26b0670..c7fa8211565d 100644
--- a/tests/expected/function-contract/interior-mutability/cell.rs
+++ b/tests/expected/function-contract/interior-mutability/cell.rs
@@ -2,46 +2,46 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-use std::cell::{Cell, OnceCell, UnsafeCell};
-use std::mem::transmute;
-
-trait ToHack<T: ?Sized> {
-    unsafe fn hack(&self) -> &T;
-}
+// ---------------------------------------------------
+//        Abstraction Breaking Functionality
+// ---------------------------------------------------
 
-impl<T: ?Sized> ToHack<T> for UnsafeCell<T> {
-    unsafe fn hack(&self) -> &T {
-        transmute(self)
-    }
-}
+use std::cell::Cell;
+use std::mem::transmute;
 
-impl<T: ?Sized> ToHack<T> for Cell<T> {
-    unsafe fn hack(&self) -> &T {
-        transmute(self)
-    }
+/// 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;
 }
 
-impl<T> ToHack<Option<T>> for OnceCell<T> {
-    unsafe fn hack(&self) -> &Option<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::requires(*unsafe{x.x.hack()} < 100)]
-#[kani::modifies(x.x.hack())]
-#[kani::ensures(|_| *unsafe{x.x.hack()} < 101)]
-fn modify(x: &InteriorMutability) {
-    x.x.set(x.x.get() + 1)
+// 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)]
+fn modify(im: &InteriorMutability) {
+    //im is an immutable reference with interior mutability
+    // valid rust methodology for getting and setting value without breaking encapsulation
+    im.x.set(im.x.get() + 1)
 }
 
 #[kani::proof_for_contract(modify)]
-fn main() {
-    let x: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) };
-    modify(&x)
+fn harness_for_modify() {
+    let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) };
+    modify(&im)
 }
diff --git a/tests/expected/function-contract/interior-mutability/oncecell.expected b/tests/expected/function-contract/interior-mutability/oncecell.expected
index d6349f472b07..482bf303b444 100644
--- a/tests/expected/function-contract/interior-mutability/oncecell.expected
+++ b/tests/expected/function-contract/interior-mutability/oncecell.expected
@@ -1,6 +1,6 @@
 assertion\
 - Status: SUCCESS\
-- Description: "|_| unsafe{ x.x.hack() }.is_some()"\
+- Description: "|_| unsafe{ im.x.expose() }.is_some()"\
 in function modify
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/oncecell.rs b/tests/expected/function-contract/interior-mutability/oncecell.rs
index 48e99eea49ad..5cb75815bd8d 100644
--- a/tests/expected/function-contract/interior-mutability/oncecell.rs
+++ b/tests/expected/function-contract/interior-mutability/oncecell.rs
@@ -2,46 +2,45 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-use std::cell::{Cell, OnceCell, UnsafeCell};
-use std::mem::transmute;
-
-trait ToHack<T: ?Sized> {
-    unsafe fn hack(&self) -> &T;
-}
+// ---------------------------------------------------
+//        Abstraction Breaking Functionality
+// ---------------------------------------------------
 
-impl<T: ?Sized> ToHack<T> for UnsafeCell<T> {
-    unsafe fn hack(&self) -> &T {
-        transmute(self)
-    }
-}
+use std::cell::OnceCell;
+use std::mem::transmute;
 
-impl<T: ?Sized> ToHack<T> for Cell<T> {
-    unsafe fn hack(&self) -> &T {
-        transmute(self)
-    }
+/// 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;
 }
 
-impl<T> ToHack<Option<T>> for OnceCell<T> {
-    unsafe fn hack(&self) -> &Option<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>,
 }
 
-#[kani::requires(unsafe{x.x.hack()}.is_none())]
-#[kani::modifies(x.x.hack())]
-#[kani::ensures(|_| unsafe{x.x.hack()}.is_some())]
-fn modify(x: &InteriorMutability) {
-    x.x.set(5).expect("")
+// 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 main() {
-    let x: InteriorMutability = InteriorMutability { x: OnceCell::new() };
-    modify(&x)
+fn harness_for_modify() {
+    let im: InteriorMutability = InteriorMutability { x: OnceCell::new() };
+    modify(&im)
 }
diff --git a/tests/expected/function-contract/interior-mutability/unsafecell.expected b/tests/expected/function-contract/interior-mutability/unsafecell.expected
index c04e2c96c0c2..29d911ad74f4 100644
--- a/tests/expected/function-contract/interior-mutability/unsafecell.expected
+++ b/tests/expected/function-contract/interior-mutability/unsafecell.expected
@@ -1,6 +1,6 @@
 assertion\
 - Status: SUCCESS\
-- Description: "|_| *unsafe{ x.x.hack() } < 101"\
+- Description: "|_| *unsafe{ im.x.expose() } < 101"\
 in function modify
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/unsafecell.rs b/tests/expected/function-contract/interior-mutability/unsafecell.rs
index fb17967fbd34..2147a2f1d34a 100644
--- a/tests/expected/function-contract/interior-mutability/unsafecell.rs
+++ b/tests/expected/function-contract/interior-mutability/unsafecell.rs
@@ -2,46 +2,45 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-use std::cell::{Cell, OnceCell, UnsafeCell};
-use std::mem::transmute;
-
-trait ToHack<T: ?Sized> {
-    unsafe fn hack(&self) -> &T;
-}
+// ---------------------------------------------------
+//        Abstraction Breaking Functionality
+// ---------------------------------------------------
 
-impl<T: ?Sized> ToHack<T> for UnsafeCell<T> {
-    unsafe fn hack(&self) -> &T {
-        transmute(self)
-    }
-}
+use std::cell::UnsafeCell;
+use std::mem::transmute;
 
-impl<T: ?Sized> ToHack<T> for Cell<T> {
-    unsafe fn hack(&self) -> &T {
-        transmute(self)
-    }
+/// 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;
 }
 
-impl<T> ToHack<Option<T>> for OnceCell<T> {
-    unsafe fn hack(&self) -> &Option<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>,
 }
 
-#[kani::requires(*unsafe{x.x.hack()} < 100)]
-#[kani::modifies(x.x.hack())]
-#[kani::ensures(|_| *unsafe{x.x.hack()} < 101)]
-fn modify(x: &InteriorMutability) {
-    unsafe { *x.x.get() += 1 }
+// 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)]
+fn modify(im: &InteriorMutability) {
+    //im is an immutable reference with interior mutability
+    unsafe { *im.x.get() += 1 }
 }
 
 #[kani::proof_for_contract(modify)]
-fn main() {
-    let x: InteriorMutability = InteriorMutability { x: UnsafeCell::new(kani::any()) };
-    modify(&x)
+fn harness_for_modify() {
+    let im: InteriorMutability = InteriorMutability { x: UnsafeCell::new(kani::any()) };
+    modify(&im)
 }

From f97140e20406c397b153be9f3dc87aeeb99df851 Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Thu, 18 Jul 2024 16:43:45 -0400
Subject: [PATCH 07/32] stub

---
 .../interior-mutability/cell_stub.expected    |  9 +++
 .../interior-mutability/cell_stub.rs          | 59 +++++++++++++++++++
 2 files changed, 68 insertions(+)
 create mode 100644 tests/expected/function-contract/interior-mutability/cell_stub.expected
 create mode 100644 tests/expected/function-contract/interior-mutability/cell_stub.rs

diff --git a/tests/expected/function-contract/interior-mutability/cell_stub.expected b/tests/expected/function-contract/interior-mutability/cell_stub.expected
new file mode 100644
index 000000000000..9d7b299422e0
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/cell_stub.expected
@@ -0,0 +1,9 @@
+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
diff --git a/tests/expected/function-contract/interior-mutability/cell_stub.rs b/tests/expected/function-contract/interior-mutability/cell_stub.rs
new file mode 100644
index 000000000000..56c04b7a2a8c
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/cell_stub.rs
@@ -0,0 +1,59 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+// ---------------------------------------------------
+//        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);
+}

From 7b96733f9df2298ca5402c52d251e3be10e86e15 Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Thu, 18 Jul 2024 16:50:46 -0400
Subject: [PATCH 08/32] more comments

---
 tests/expected/function-contract/interior-mutability/cell.rs   | 2 ++
 .../function-contract/interior-mutability/cell_stub.rs         | 3 +++
 .../expected/function-contract/interior-mutability/oncecell.rs | 2 ++
 .../function-contract/interior-mutability/unsafecell.rs        | 2 ++
 4 files changed, 9 insertions(+)

diff --git a/tests/expected/function-contract/interior-mutability/cell.rs b/tests/expected/function-contract/interior-mutability/cell.rs
index c7fa8211565d..84ef47476aab 100644
--- a/tests/expected/function-contract/interior-mutability/cell.rs
+++ b/tests/expected/function-contract/interior-mutability/cell.rs
@@ -2,6 +2,8 @@
 // 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
 // ---------------------------------------------------
diff --git a/tests/expected/function-contract/interior-mutability/cell_stub.rs b/tests/expected/function-contract/interior-mutability/cell_stub.rs
index 56c04b7a2a8c..98fd0934627b 100644
--- a/tests/expected/function-contract/interior-mutability/cell_stub.rs
+++ b/tests/expected/function-contract/interior-mutability/cell_stub.rs
@@ -2,6 +2,9 @@
 // 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
 // ---------------------------------------------------
diff --git a/tests/expected/function-contract/interior-mutability/oncecell.rs b/tests/expected/function-contract/interior-mutability/oncecell.rs
index 5cb75815bd8d..1423edfb1d27 100644
--- a/tests/expected/function-contract/interior-mutability/oncecell.rs
+++ b/tests/expected/function-contract/interior-mutability/oncecell.rs
@@ -2,6 +2,8 @@
 // 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
 // ---------------------------------------------------
diff --git a/tests/expected/function-contract/interior-mutability/unsafecell.rs b/tests/expected/function-contract/interior-mutability/unsafecell.rs
index 2147a2f1d34a..d09b199f8c89 100644
--- a/tests/expected/function-contract/interior-mutability/unsafecell.rs
+++ b/tests/expected/function-contract/interior-mutability/unsafecell.rs
@@ -2,6 +2,8 @@
 // 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
 // ---------------------------------------------------

From fae9ff2e783bf7f25d73591c5c009f68f61affd7 Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Fri, 19 Jul 2024 12:39:13 -0400
Subject: [PATCH 09/32] fix test

---
 .../interior-mutability/cell_stub.expected                | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/tests/expected/function-contract/interior-mutability/cell_stub.expected b/tests/expected/function-contract/interior-mutability/cell_stub.expected
index 9d7b299422e0..e82a3c778305 100644
--- a/tests/expected/function-contract/interior-mutability/cell_stub.expected
+++ b/tests/expected/function-contract/interior-mutability/cell_stub.expected
@@ -1,9 +1,13 @@
 assertion\
 - Status: SUCCESS\
-- Description: "|_| old(*unsafe{ im.x.expose() } + *unsafe{ im.x.expose() }) == *unsafe{ im.x.expose() }"\
+- 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() }"\
+- Description: "|_|
+old(*unsafe{ im.x.expose() } + *unsafe{ im.x.expose() } +\
+*unsafe{ im.x.expose() } + *unsafe{ im.x.expose() }) ==\
+*unsafe{ im.x.expose() }"\
 
 VERIFICATION:- SUCCESSFUL

From 600a0f10e007961e0dc40b2ac71c3ef3f6e9024d Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Fri, 19 Jul 2024 15:39:57 -0400
Subject: [PATCH 10/32] rfc update

---
 rfc/src/rfcs/0009-function-contracts.md | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/rfc/src/rfcs/0009-function-contracts.md b/rfc/src/rfcs/0009-function-contracts.md
index a8bd7bf66041..865237fbe966 100644
--- a/rfc/src/rfcs/0009-function-contracts.md
+++ b/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
 

From 7a0a55468c4e2632c2da9e54ab4e02c1f1bae3f7 Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Mon, 22 Jul 2024 15:06:00 -0400
Subject: [PATCH 11/32] unsafecell and cell can be reached through public api

---
 .../interior-mutability/api/cell.expected     |  6 ++++
 .../interior-mutability/api/cell.rs           | 28 +++++++++++++++++++
 .../api/unsafecell.expected                   |  6 ++++
 .../interior-mutability/api/unsafecell.rs     | 25 +++++++++++++++++
 .../{ => transmute}/cell.expected             |  0
 .../{ => transmute}/cell.rs                   |  0
 .../{ => transmute}/cell_stub.expected        |  0
 .../{ => transmute}/cell_stub.rs              |  0
 .../{ => transmute}/oncecell.expected         |  0
 .../{ => transmute}/oncecell.rs               |  0
 .../{ => transmute}/unsafecell.expected       |  0
 .../{ => transmute}/unsafecell.rs             |  0
 12 files changed, 65 insertions(+)
 create mode 100644 tests/expected/function-contract/interior-mutability/api/cell.expected
 create mode 100644 tests/expected/function-contract/interior-mutability/api/cell.rs
 create mode 100644 tests/expected/function-contract/interior-mutability/api/unsafecell.expected
 create mode 100644 tests/expected/function-contract/interior-mutability/api/unsafecell.rs
 rename tests/expected/function-contract/interior-mutability/{ => transmute}/cell.expected (100%)
 rename tests/expected/function-contract/interior-mutability/{ => transmute}/cell.rs (100%)
 rename tests/expected/function-contract/interior-mutability/{ => transmute}/cell_stub.expected (100%)
 rename tests/expected/function-contract/interior-mutability/{ => transmute}/cell_stub.rs (100%)
 rename tests/expected/function-contract/interior-mutability/{ => transmute}/oncecell.expected (100%)
 rename tests/expected/function-contract/interior-mutability/{ => transmute}/oncecell.rs (100%)
 rename tests/expected/function-contract/interior-mutability/{ => transmute}/unsafecell.expected (100%)
 rename tests/expected/function-contract/interior-mutability/{ => transmute}/unsafecell.rs (100%)

diff --git a/tests/expected/function-contract/interior-mutability/api/cell.expected b/tests/expected/function-contract/interior-mutability/api/cell.expected
new file mode 100644
index 000000000000..d9b0f5d51e5c
--- /dev/null
+++ b/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
diff --git a/tests/expected/function-contract/interior-mutability/api/cell.rs b/tests/expected/function-contract/interior-mutability/api/cell.rs
new file mode 100644
index 000000000000..49609384d4e8
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/api/cell.rs
@@ -0,0 +1,28 @@
+// 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)]
+fn modify(im: &InteriorMutability) {
+    //im is an immutable reference with interior mutability
+    // 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)
+}
diff --git a/tests/expected/function-contract/interior-mutability/api/unsafecell.expected b/tests/expected/function-contract/interior-mutability/api/unsafecell.expected
new file mode 100644
index 000000000000..1646a8a78e7f
--- /dev/null
+++ b/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
diff --git a/tests/expected/function-contract/interior-mutability/api/unsafecell.rs b/tests/expected/function-contract/interior-mutability/api/unsafecell.rs
new file mode 100644
index 000000000000..07f528ec69fd
--- /dev/null
+++ b/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)]
+fn modify(im: &InteriorMutability) {
+    //im is an immutable reference with interior mutability
+    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)
+}
diff --git a/tests/expected/function-contract/interior-mutability/cell.expected b/tests/expected/function-contract/interior-mutability/transmute/cell.expected
similarity index 100%
rename from tests/expected/function-contract/interior-mutability/cell.expected
rename to tests/expected/function-contract/interior-mutability/transmute/cell.expected
diff --git a/tests/expected/function-contract/interior-mutability/cell.rs b/tests/expected/function-contract/interior-mutability/transmute/cell.rs
similarity index 100%
rename from tests/expected/function-contract/interior-mutability/cell.rs
rename to tests/expected/function-contract/interior-mutability/transmute/cell.rs
diff --git a/tests/expected/function-contract/interior-mutability/cell_stub.expected b/tests/expected/function-contract/interior-mutability/transmute/cell_stub.expected
similarity index 100%
rename from tests/expected/function-contract/interior-mutability/cell_stub.expected
rename to tests/expected/function-contract/interior-mutability/transmute/cell_stub.expected
diff --git a/tests/expected/function-contract/interior-mutability/cell_stub.rs b/tests/expected/function-contract/interior-mutability/transmute/cell_stub.rs
similarity index 100%
rename from tests/expected/function-contract/interior-mutability/cell_stub.rs
rename to tests/expected/function-contract/interior-mutability/transmute/cell_stub.rs
diff --git a/tests/expected/function-contract/interior-mutability/oncecell.expected b/tests/expected/function-contract/interior-mutability/transmute/oncecell.expected
similarity index 100%
rename from tests/expected/function-contract/interior-mutability/oncecell.expected
rename to tests/expected/function-contract/interior-mutability/transmute/oncecell.expected
diff --git a/tests/expected/function-contract/interior-mutability/oncecell.rs b/tests/expected/function-contract/interior-mutability/transmute/oncecell.rs
similarity index 100%
rename from tests/expected/function-contract/interior-mutability/oncecell.rs
rename to tests/expected/function-contract/interior-mutability/transmute/oncecell.rs
diff --git a/tests/expected/function-contract/interior-mutability/unsafecell.expected b/tests/expected/function-contract/interior-mutability/transmute/unsafecell.expected
similarity index 100%
rename from tests/expected/function-contract/interior-mutability/unsafecell.expected
rename to tests/expected/function-contract/interior-mutability/transmute/unsafecell.expected
diff --git a/tests/expected/function-contract/interior-mutability/unsafecell.rs b/tests/expected/function-contract/interior-mutability/transmute/unsafecell.rs
similarity index 100%
rename from tests/expected/function-contract/interior-mutability/unsafecell.rs
rename to tests/expected/function-contract/interior-mutability/transmute/unsafecell.rs

From e704958ae41fe5a985c2f69b4b4b885ee9b0b087 Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Mon, 22 Jul 2024 16:01:04 -0400
Subject: [PATCH 12/32] triple slash for comments

---
 .../interior-mutability/api/cell.rs           | 11 ++++----
 .../interior-mutability/api/unsafecell.rs     |  6 ++---
 .../interior-mutability/transmute/cell.rs     | 25 +++++++++----------
 .../transmute/cell_stub.rs                    | 21 ++++++++--------
 .../interior-mutability/transmute/oncecell.rs | 23 ++++++++---------
 .../transmute/unsafecell.rs                   | 23 ++++++++---------
 6 files changed, 52 insertions(+), 57 deletions(-)

diff --git a/tests/expected/function-contract/interior-mutability/api/cell.rs b/tests/expected/function-contract/interior-mutability/api/cell.rs
index 49609384d4e8..b5d95907e0d2 100644
--- a/tests/expected/function-contract/interior-mutability/api/cell.rs
+++ b/tests/expected/function-contract/interior-mutability/api/cell.rs
@@ -2,22 +2,21 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-// Mutating Cell via as_ptr in contracts
-
+/// Mutating Cell via as_ptr in contracts
 use std::cell::Cell;
 
-// This struct is contains Cell which can be mutated
+/// 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
+/// 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) {
-    //im is an immutable reference with interior mutability
-    // valid rust methodology for getting and setting value without breaking encapsulation
+    /// valid rust methodology for getting and setting value without breaking encapsulation
     im.x.set(im.x.get() + 1)
 }
 
diff --git a/tests/expected/function-contract/interior-mutability/api/unsafecell.rs b/tests/expected/function-contract/interior-mutability/api/unsafecell.rs
index 07f528ec69fd..5c15c8172678 100644
--- a/tests/expected/function-contract/interior-mutability/api/unsafecell.rs
+++ b/tests/expected/function-contract/interior-mutability/api/unsafecell.rs
@@ -4,17 +4,17 @@
 
 use std::cell::UnsafeCell;
 
-// This struct is contains UnsafeCell which can be mutated
+/// 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
+/// 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) {
-    //im is an immutable reference with interior mutability
     unsafe { *im.x.get() += 1 }
 }
 
diff --git a/tests/expected/function-contract/interior-mutability/transmute/cell.rs b/tests/expected/function-contract/interior-mutability/transmute/cell.rs
index 84ef47476aab..a03db1fa0ef3 100644
--- a/tests/expected/function-contract/interior-mutability/transmute/cell.rs
+++ b/tests/expected/function-contract/interior-mutability/transmute/cell.rs
@@ -2,12 +2,11 @@
 // 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
-// ---------------------------------------------------
+/// 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;
 
@@ -16,29 +15,29 @@ 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
+/// 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
-// ---------------------------------------------------
+/// ---------------------------------------------------
+///                      Test Case
+/// ---------------------------------------------------
 
-// This struct is contains Cell which can be mutated
+/// 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()
+/// 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) {
-    //im is an immutable reference with interior mutability
-    // valid rust methodology for getting and setting value without breaking encapsulation
+    /// valid rust methodology for getting and setting value without breaking encapsulation
     im.x.set(im.x.get() + 1)
 }
 
diff --git a/tests/expected/function-contract/interior-mutability/transmute/cell_stub.rs b/tests/expected/function-contract/interior-mutability/transmute/cell_stub.rs
index 98fd0934627b..4b9469ccfb3d 100644
--- a/tests/expected/function-contract/interior-mutability/transmute/cell_stub.rs
+++ b/tests/expected/function-contract/interior-mutability/transmute/cell_stub.rs
@@ -2,13 +2,12 @@
 // 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
-// ---------------------------------------------------
+/// 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;
 
@@ -17,18 +16,18 @@ 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
+/// 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
-// ---------------------------------------------------
+/// ---------------------------------------------------
+///                      Test Case
+/// ---------------------------------------------------
 
-// This struct is contains Cell which can be mutated
+/// This struct is contains Cell which can be mutated
 struct InteriorMutability {
     x: Cell<u32>,
 }
diff --git a/tests/expected/function-contract/interior-mutability/transmute/oncecell.rs b/tests/expected/function-contract/interior-mutability/transmute/oncecell.rs
index 1423edfb1d27..d2bb168eb069 100644
--- a/tests/expected/function-contract/interior-mutability/transmute/oncecell.rs
+++ b/tests/expected/function-contract/interior-mutability/transmute/oncecell.rs
@@ -2,12 +2,11 @@
 // 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
-// ---------------------------------------------------
+/// 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;
 
@@ -16,28 +15,28 @@ 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
+/// 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
-// ---------------------------------------------------
+/// ---------------------------------------------------
+///                      Test Case
+/// ---------------------------------------------------
 
-// This struct is contains OnceCell which can be mutated
+/// 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()
+/// 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
+    /// method for setting value in OnceCell without breaking encapsulation
     im.x.set(5).expect("")
 }
 
diff --git a/tests/expected/function-contract/interior-mutability/transmute/unsafecell.rs b/tests/expected/function-contract/interior-mutability/transmute/unsafecell.rs
index d09b199f8c89..2a2cf6d1f5bd 100644
--- a/tests/expected/function-contract/interior-mutability/transmute/unsafecell.rs
+++ b/tests/expected/function-contract/interior-mutability/transmute/unsafecell.rs
@@ -2,12 +2,11 @@
 // 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
-// ---------------------------------------------------
+/// 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;
 
@@ -16,28 +15,28 @@ 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
+/// 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
-// ---------------------------------------------------
+/// ---------------------------------------------------
+///                      Test Case
+/// ---------------------------------------------------
 
-// This struct is contains UnsafeCell which can be mutated
+/// 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()
+/// 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) {
-    //im is an immutable reference with interior mutability
     unsafe { *im.x.get() += 1 }
 }
 

From 382e8feccab1731ac4faa449ecbef750134feb7a Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Tue, 23 Jul 2024 17:06:42 -0400
Subject: [PATCH 13/32] more tests

---
 .../interior-mutability/api/cell.rs           |  2 +-
 .../api/cell_stub.expected                    |  9 +++
 .../interior-mutability/api/cell_stub.rs      | 41 +++++++++++++
 .../interior-mutability/transmute/cell.rs     |  2 +-
 .../transmute/cell_stub.expected              | 13 ----
 .../transmute/cell_stub.rs                    | 61 -------------------
 .../interior-mutability/transmute/oncecell.rs |  2 +-
 .../whole-struct/cell.expected                |  6 ++
 .../interior-mutability/whole-struct/cell.rs  | 27 ++++++++
 .../whole-struct/oncecell.expected            |  6 ++
 .../whole-struct/oncecell.rs                  | 26 ++++++++
 .../whole-struct/refcell.expected             |  6 ++
 .../whole-struct/refcell.rs                   | 27 ++++++++
 .../whole-struct/unsafecell.expected          |  6 ++
 .../whole-struct/unsafecell.rs                | 26 ++++++++
 15 files changed, 183 insertions(+), 77 deletions(-)
 create mode 100644 tests/expected/function-contract/interior-mutability/api/cell_stub.expected
 create mode 100644 tests/expected/function-contract/interior-mutability/api/cell_stub.rs
 delete mode 100644 tests/expected/function-contract/interior-mutability/transmute/cell_stub.expected
 delete mode 100644 tests/expected/function-contract/interior-mutability/transmute/cell_stub.rs
 create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/cell.expected
 create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/cell.rs
 create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/oncecell.expected
 create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs
 create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/refcell.expected
 create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs
 create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.expected
 create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs

diff --git a/tests/expected/function-contract/interior-mutability/api/cell.rs b/tests/expected/function-contract/interior-mutability/api/cell.rs
index b5d95907e0d2..aa62b1479ee3 100644
--- a/tests/expected/function-contract/interior-mutability/api/cell.rs
+++ b/tests/expected/function-contract/interior-mutability/api/cell.rs
@@ -16,7 +16,7 @@ struct InteriorMutability {
 #[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
+    // valid rust methodology for getting and setting value without breaking encapsulation
     im.x.set(im.x.get() + 1)
 }
 
diff --git a/tests/expected/function-contract/interior-mutability/api/cell_stub.expected b/tests/expected/function-contract/interior-mutability/api/cell_stub.expected
new file mode 100644
index 000000000000..b8da35411e53
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/api/cell_stub.expected
@@ -0,0 +1,9 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| old(im.x.get() + im.x.get()) == im.x.get()"\
+
+assertion\
+- Status: SUCCESS\
+- Description: "|_| old(im.x.get() + im.x.get() + im.x.get() + im.x.get()) == im.x.get()"\
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/api/cell_stub.rs b/tests/expected/function-contract/interior-mutability/api/cell_stub.rs
new file mode 100644
index 000000000000..7313666cccb1
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/api/cell_stub.rs
@@ -0,0 +1,41 @@
+// 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
+
+use std::cell::Cell;
+
+/// This struct is contains Cell which can be mutated
+struct InteriorMutability {
+    x: Cell<u32>,
+}
+
+#[kani::ensures(|_| old(im.x.get() + im.x.get()) == im.x.get())]
+#[kani::requires(im.x.get() < 100)]
+#[kani::modifies(im.x.as_ptr())]
+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(im.x.get() + im.x.get() + im.x.get() + im.x.get()) == im.x.get())]
+#[kani::requires(im.x.get() < 50)]
+#[kani::modifies(im.x.as_ptr())]
+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);
+}
diff --git a/tests/expected/function-contract/interior-mutability/transmute/cell.rs b/tests/expected/function-contract/interior-mutability/transmute/cell.rs
index a03db1fa0ef3..308af5aa8b77 100644
--- a/tests/expected/function-contract/interior-mutability/transmute/cell.rs
+++ b/tests/expected/function-contract/interior-mutability/transmute/cell.rs
@@ -37,7 +37,7 @@ struct InteriorMutability {
 #[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
+    // valid rust methodology for getting and setting value without breaking encapsulation
     im.x.set(im.x.get() + 1)
 }
 
diff --git a/tests/expected/function-contract/interior-mutability/transmute/cell_stub.expected b/tests/expected/function-contract/interior-mutability/transmute/cell_stub.expected
deleted file mode 100644
index e82a3c778305..000000000000
--- a/tests/expected/function-contract/interior-mutability/transmute/cell_stub.expected
+++ /dev/null
@@ -1,13 +0,0 @@
-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
diff --git a/tests/expected/function-contract/interior-mutability/transmute/cell_stub.rs b/tests/expected/function-contract/interior-mutability/transmute/cell_stub.rs
deleted file mode 100644
index 4b9469ccfb3d..000000000000
--- a/tests/expected/function-contract/interior-mutability/transmute/cell_stub.rs
+++ /dev/null
@@ -1,61 +0,0 @@
-// 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);
-}
diff --git a/tests/expected/function-contract/interior-mutability/transmute/oncecell.rs b/tests/expected/function-contract/interior-mutability/transmute/oncecell.rs
index d2bb168eb069..1c752f3ce946 100644
--- a/tests/expected/function-contract/interior-mutability/transmute/oncecell.rs
+++ b/tests/expected/function-contract/interior-mutability/transmute/oncecell.rs
@@ -36,7 +36,7 @@ struct InteriorMutability {
 #[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
+    // method for setting value in OnceCell without breaking encapsulation
     im.x.set(5).expect("")
 }
 
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/cell.expected b/tests/expected/function-contract/interior-mutability/whole-struct/cell.expected
new file mode 100644
index 000000000000..d9b0f5d51e5c
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/cell.expected
@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| im.x.get() < 101"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs
new file mode 100644
index 000000000000..bc09c1b0fc87
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs
@@ -0,0 +1,27 @@
+// 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
+
+use std::cell::Cell;
+
+/// This struct is contains Cell which can be mutated
+struct InteriorMutability {
+    x: Cell<u32>,
+}
+
+#[kani::requires(im.x.get() < 100)]
+#[kani::modifies(&im.x)]
+#[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)
+}
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.expected b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.expected
new file mode 100644
index 000000000000..a367bcd9fb95
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.expected
@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| im.x.get().is_some()"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs
new file mode 100644
index 000000000000..45a1cc69692e
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs
@@ -0,0 +1,26 @@
+// 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
+
+use std::cell::OnceCell;
+
+/// This struct is contains OnceCell which can be mutated
+struct InteriorMutability {
+    x: OnceCell<u32>,
+}
+
+#[kani::requires(im.x.get().is_none())]
+#[kani::modifies(&im.x)]
+#[kani::ensures(|_| im.x.get().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)
+}
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/refcell.expected b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.expected
new file mode 100644
index 000000000000..225c290a171e
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.expected
@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| unsafe{ *im.x.as_ptr() } < 101"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs
new file mode 100644
index 000000000000..fc9c4848b3c0
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs
@@ -0,0 +1,27 @@
+// 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 RefCell used as interior mutability in an immutable struct
+
+use std::cell::RefCell;
+
+/// This struct is contains Cell which can be mutated
+struct InteriorMutability {
+    x: RefCell<u32>,
+}
+
+#[kani::requires(unsafe{*im.x.as_ptr()} < 100)]
+#[kani::modifies(&im.x)]
+#[kani::ensures(|_| unsafe{*im.x.as_ptr()} < 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.replace_with(|&mut old| old + 1);
+}
+
+#[kani::proof_for_contract(modify)]
+fn harness_for_modify() {
+    let im: InteriorMutability = InteriorMutability { x: RefCell::new(kani::any()) };
+    modify(&im)
+}
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.expected b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.expected
new file mode 100644
index 000000000000..1646a8a78e7f
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.expected
@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| unsafe{ *im.x.get() } < 101"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs
new file mode 100644
index 000000000000..b32cdb33d4d7
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs
@@ -0,0 +1,26 @@
+// 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
+
+use std::cell::UnsafeCell;
+
+/// This struct is contains UnsafeCell which can be mutated
+struct InteriorMutability {
+    x: UnsafeCell<u32>,
+}
+
+#[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)
+}

From 39cdc44033d4be6b017b125c44f505b840e5b9b4 Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Tue, 23 Jul 2024 17:10:10 -0400
Subject: [PATCH 14/32] fmt

---
 .../function-contract/interior-mutability/api/cell_stub.rs       | 1 -
 .../function-contract/interior-mutability/whole-struct/cell.rs   | 1 -
 .../interior-mutability/whole-struct/oncecell.rs                 | 1 -
 .../interior-mutability/whole-struct/refcell.rs                  | 1 -
 .../interior-mutability/whole-struct/unsafecell.rs               | 1 -
 5 files changed, 5 deletions(-)

diff --git a/tests/expected/function-contract/interior-mutability/api/cell_stub.rs b/tests/expected/function-contract/interior-mutability/api/cell_stub.rs
index 7313666cccb1..9e2b1ff52975 100644
--- a/tests/expected/function-contract/interior-mutability/api/cell_stub.rs
+++ b/tests/expected/function-contract/interior-mutability/api/cell_stub.rs
@@ -4,7 +4,6 @@
 
 /// 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
-
 use std::cell::Cell;
 
 /// This struct is contains Cell which can be mutated
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs
index bc09c1b0fc87..bb2f136b64a6 100644
--- a/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs
@@ -3,7 +3,6 @@
 // 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
-
 use std::cell::Cell;
 
 /// This struct is contains Cell which can be mutated
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs
index 45a1cc69692e..d6fa23f7ec05 100644
--- a/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs
@@ -3,7 +3,6 @@
 // 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
-
 use std::cell::OnceCell;
 
 /// This struct is contains OnceCell which can be mutated
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs
index fc9c4848b3c0..d83300aa4592 100644
--- a/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs
@@ -3,7 +3,6 @@
 // kani-flags: -Zfunction-contracts
 
 /// The objective of this test is to check the modification of a RefCell used as interior mutability in an immutable struct
-
 use std::cell::RefCell;
 
 /// This struct is contains Cell which can be mutated
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs
index b32cdb33d4d7..6cef4d62ce44 100644
--- a/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs
@@ -3,7 +3,6 @@
 // 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
-
 use std::cell::UnsafeCell;
 
 /// This struct is contains UnsafeCell which can be mutated

From 03f3d6d1f43ffb2d577928d682d52d09621bf796 Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Wed, 24 Jul 2024 12:27:29 -0400
Subject: [PATCH 15/32] fix tests

---
 .../interior-mutability/api/cell.rs           |  2 -
 .../interior-mutability/api/unsafecell.rs     |  1 -
 .../transmute/oncecell.expected               |  6 ---
 .../interior-mutability/transmute/oncecell.rs | 47 -------------------
 .../interior-mutability/whole-struct/cell.rs  |  1 -
 .../whole-struct/oncecell.rs                  |  1 -
 .../whole-struct/refcell.rs                   |  1 -
 .../transmute/cell.expected                   |  2 +-
 .../transmute/cell.rs                         | 23 ++++-----
 .../transmute/unsafecell.expected             |  2 +-
 .../transmute/unsafecell.rs                   | 23 ++++-----
 11 files changed, 18 insertions(+), 91 deletions(-)
 delete mode 100644 tests/expected/function-contract/interior-mutability/transmute/oncecell.expected
 delete mode 100644 tests/expected/function-contract/interior-mutability/transmute/oncecell.rs
 rename tests/expected/function-contract/{interior-mutability => }/transmute/cell.expected (58%)
 rename tests/expected/function-contract/{interior-mutability => }/transmute/cell.rs (62%)
 rename tests/expected/function-contract/{interior-mutability => }/transmute/unsafecell.expected (58%)
 rename tests/expected/function-contract/{interior-mutability => }/transmute/unsafecell.rs (60%)

diff --git a/tests/expected/function-contract/interior-mutability/api/cell.rs b/tests/expected/function-contract/interior-mutability/api/cell.rs
index aa62b1479ee3..c8dbf39bb159 100644
--- a/tests/expected/function-contract/interior-mutability/api/cell.rs
+++ b/tests/expected/function-contract/interior-mutability/api/cell.rs
@@ -10,13 +10,11 @@ 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)
 }
 
diff --git a/tests/expected/function-contract/interior-mutability/api/unsafecell.rs b/tests/expected/function-contract/interior-mutability/api/unsafecell.rs
index 5c15c8172678..18c9602a69c3 100644
--- a/tests/expected/function-contract/interior-mutability/api/unsafecell.rs
+++ b/tests/expected/function-contract/interior-mutability/api/unsafecell.rs
@@ -9,7 +9,6 @@ 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)]
diff --git a/tests/expected/function-contract/interior-mutability/transmute/oncecell.expected b/tests/expected/function-contract/interior-mutability/transmute/oncecell.expected
deleted file mode 100644
index 482bf303b444..000000000000
--- a/tests/expected/function-contract/interior-mutability/transmute/oncecell.expected
+++ /dev/null
@@ -1,6 +0,0 @@
-assertion\
-- Status: SUCCESS\
-- Description: "|_| unsafe{ im.x.expose() }.is_some()"\
-in function modify
-
-VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/transmute/oncecell.rs b/tests/expected/function-contract/interior-mutability/transmute/oncecell.rs
deleted file mode 100644
index 1c752f3ce946..000000000000
--- a/tests/expected/function-contract/interior-mutability/transmute/oncecell.rs
+++ /dev/null
@@ -1,47 +0,0 @@
-// 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)
-}
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs
index bb2f136b64a6..a67aefa356fc 100644
--- a/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs
@@ -15,7 +15,6 @@ struct InteriorMutability {
 #[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)
 }
 
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs
index d6fa23f7ec05..081de79adecf 100644
--- a/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs
@@ -14,7 +14,6 @@ struct InteriorMutability {
 #[kani::modifies(&im.x)]
 #[kani::ensures(|_| im.x.get().is_some())]
 fn modify(im: &InteriorMutability) {
-    // method for setting value in OnceCell without breaking encapsulation
     im.x.set(5).expect("")
 }
 
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs
index d83300aa4592..df38d277f200 100644
--- a/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs
@@ -15,7 +15,6 @@ struct InteriorMutability {
 #[kani::ensures(|_| unsafe{*im.x.as_ptr()} < 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.replace_with(|&mut old| old + 1);
 }
 
diff --git a/tests/expected/function-contract/interior-mutability/transmute/cell.expected b/tests/expected/function-contract/transmute/cell.expected
similarity index 58%
rename from tests/expected/function-contract/interior-mutability/transmute/cell.expected
rename to tests/expected/function-contract/transmute/cell.expected
index 29d911ad74f4..da8fb418724e 100644
--- a/tests/expected/function-contract/interior-mutability/transmute/cell.expected
+++ b/tests/expected/function-contract/transmute/cell.expected
@@ -1,6 +1,6 @@
 assertion\
 - Status: SUCCESS\
-- Description: "|_| *unsafe{ im.x.expose() } < 101"\
+- Description: "|_| *unsafe{ x.expose() } < 101"\
 in function modify
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/transmute/cell.rs b/tests/expected/function-contract/transmute/cell.rs
similarity index 62%
rename from tests/expected/function-contract/interior-mutability/transmute/cell.rs
rename to tests/expected/function-contract/transmute/cell.rs
index 308af5aa8b77..9a5c4f6a3161 100644
--- a/tests/expected/function-contract/interior-mutability/transmute/cell.rs
+++ b/tests/expected/function-contract/transmute/cell.rs
@@ -2,7 +2,7 @@
 // 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
+/// This is a valid but not recommended alternative to havocing Cell
 
 /// ---------------------------------------------------
 ///        Abstraction Breaking Functionality
@@ -26,23 +26,16 @@ impl<T: ?Sized> Exposeable<T> for Cell<T> {
 ///                      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) {
+#[kani::requires(*unsafe{x.expose()} < 100)]
+#[kani::modifies(x.expose())]
+#[kani::ensures(|_| *unsafe{x.expose()} < 101)]
+fn modify(x: &Cell<u32>) {
     // valid rust methodology for getting and setting value without breaking encapsulation
-    im.x.set(im.x.get() + 1)
+    x.set(x.get() + 1)
 }
 
 #[kani::proof_for_contract(modify)]
 fn harness_for_modify() {
-    let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) };
-    modify(&im)
+    let x = Cell::new(kani::any());
+    modify(&x)
 }
diff --git a/tests/expected/function-contract/interior-mutability/transmute/unsafecell.expected b/tests/expected/function-contract/transmute/unsafecell.expected
similarity index 58%
rename from tests/expected/function-contract/interior-mutability/transmute/unsafecell.expected
rename to tests/expected/function-contract/transmute/unsafecell.expected
index 29d911ad74f4..da8fb418724e 100644
--- a/tests/expected/function-contract/interior-mutability/transmute/unsafecell.expected
+++ b/tests/expected/function-contract/transmute/unsafecell.expected
@@ -1,6 +1,6 @@
 assertion\
 - Status: SUCCESS\
-- Description: "|_| *unsafe{ im.x.expose() } < 101"\
+- Description: "|_| *unsafe{ x.expose() } < 101"\
 in function modify
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/transmute/unsafecell.rs b/tests/expected/function-contract/transmute/unsafecell.rs
similarity index 60%
rename from tests/expected/function-contract/interior-mutability/transmute/unsafecell.rs
rename to tests/expected/function-contract/transmute/unsafecell.rs
index 2a2cf6d1f5bd..c018b8b8912a 100644
--- a/tests/expected/function-contract/interior-mutability/transmute/unsafecell.rs
+++ b/tests/expected/function-contract/transmute/unsafecell.rs
@@ -2,7 +2,7 @@
 // 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
+/// This is a valid but not recommended alternative to havocing UnsafeCell
 
 /// ---------------------------------------------------
 ///        Abstraction Breaking Functionality
@@ -26,22 +26,15 @@ impl<T: ?Sized> Exposeable<T> for UnsafeCell<T> {
 ///                      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::requires(*unsafe{x.expose()} < 100)]
+#[kani::modifies(x.expose())]
+#[kani::ensures(|_| *unsafe{x.expose()} < 101)]
+fn modify(x: &UnsafeCell<u32>) {
+    unsafe { *x.get() += 1 }
 }
 
 #[kani::proof_for_contract(modify)]
 fn harness_for_modify() {
-    let im: InteriorMutability = InteriorMutability { x: UnsafeCell::new(kani::any()) };
-    modify(&im)
+    let x = UnsafeCell::new(kani::any());
+    modify(&x)
 }

From 8925ffb6daf2550f0b9503cb17aba20e7533153a Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Wed, 24 Jul 2024 13:06:18 -0400
Subject: [PATCH 16/32] comments

---
 rfc/src/rfcs/0009-function-contracts.md         | 17 -----------------
 .../function-contract/transmute/cell.rs         |  1 +
 .../function-contract/transmute/unsafecell.rs   |  1 +
 3 files changed, 2 insertions(+), 17 deletions(-)

diff --git a/rfc/src/rfcs/0009-function-contracts.md b/rfc/src/rfcs/0009-function-contracts.md
index 865237fbe966..7a60e295b5eb 100644
--- a/rfc/src/rfcs/0009-function-contracts.md
+++ b/rfc/src/rfcs/0009-function-contracts.md
@@ -706,23 +706,6 @@ 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
 
 <!-- For Developers -->
diff --git a/tests/expected/function-contract/transmute/cell.rs b/tests/expected/function-contract/transmute/cell.rs
index 9a5c4f6a3161..4616b090a5d6 100644
--- a/tests/expected/function-contract/transmute/cell.rs
+++ b/tests/expected/function-contract/transmute/cell.rs
@@ -3,6 +3,7 @@
 // kani-flags: -Zfunction-contracts
 
 /// This is a valid but not recommended alternative to havocing Cell
+/// Only done for test purposes
 
 /// ---------------------------------------------------
 ///        Abstraction Breaking Functionality
diff --git a/tests/expected/function-contract/transmute/unsafecell.rs b/tests/expected/function-contract/transmute/unsafecell.rs
index c018b8b8912a..988e0312fea8 100644
--- a/tests/expected/function-contract/transmute/unsafecell.rs
+++ b/tests/expected/function-contract/transmute/unsafecell.rs
@@ -3,6 +3,7 @@
 // kani-flags: -Zfunction-contracts
 
 /// This is a valid but not recommended alternative to havocing UnsafeCell
+/// Only done for test purposes
 
 /// ---------------------------------------------------
 ///        Abstraction Breaking Functionality

From 519fe5c6b19d5dbd3ab3b8244ab905c8ea9e15ed Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Wed, 24 Jul 2024 13:07:12 -0400
Subject: [PATCH 17/32] comments

---
 rfc/src/rfcs/0009-function-contracts.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/rfc/src/rfcs/0009-function-contracts.md b/rfc/src/rfcs/0009-function-contracts.md
index 7a60e295b5eb..a8bd7bf66041 100644
--- a/rfc/src/rfcs/0009-function-contracts.md
+++ b/rfc/src/rfcs/0009-function-contracts.md
@@ -706,6 +706,7 @@ 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).
 
+
 ## Open questions
 
 <!-- For Developers -->

From 2126d79bfa547a11c03a72b63756cf07eefde1f9 Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Thu, 25 Jul 2024 15:27:12 -0400
Subject: [PATCH 18/32] add explanation in docs

---
 .../src/rust-feature-support/interior-mutability.md | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 docs/src/rust-feature-support/interior-mutability.md

diff --git a/docs/src/rust-feature-support/interior-mutability.md b/docs/src/rust-feature-support/interior-mutability.md
new file mode 100644
index 000000000000..e18fa6e6bdc1
--- /dev/null
+++ b/docs/src/rust-feature-support/interior-mutability.md
@@ -0,0 +1,13 @@
+# 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.
\ No newline at end of file

From 3fb40fce8d79545a5e587ee4a7699ac689f59745 Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Fri, 26 Jul 2024 13:23:50 -0400
Subject: [PATCH 19/32] delete

---
 .../interior-mutability.md                    | 13 ------
 .../function-contract/transmute/cell.expected |  6 ---
 .../function-contract/transmute/cell.rs       | 42 -------------------
 .../transmute/unsafecell.expected             |  6 ---
 .../function-contract/transmute/unsafecell.rs | 41 ------------------
 5 files changed, 108 deletions(-)
 delete mode 100644 docs/src/rust-feature-support/interior-mutability.md
 delete mode 100644 tests/expected/function-contract/transmute/cell.expected
 delete mode 100644 tests/expected/function-contract/transmute/cell.rs
 delete mode 100644 tests/expected/function-contract/transmute/unsafecell.expected
 delete mode 100644 tests/expected/function-contract/transmute/unsafecell.rs

diff --git a/docs/src/rust-feature-support/interior-mutability.md b/docs/src/rust-feature-support/interior-mutability.md
deleted file mode 100644
index e18fa6e6bdc1..000000000000
--- a/docs/src/rust-feature-support/interior-mutability.md
+++ /dev/null
@@ -1,13 +0,0 @@
-# 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.
\ No newline at end of file
diff --git a/tests/expected/function-contract/transmute/cell.expected b/tests/expected/function-contract/transmute/cell.expected
deleted file mode 100644
index da8fb418724e..000000000000
--- a/tests/expected/function-contract/transmute/cell.expected
+++ /dev/null
@@ -1,6 +0,0 @@
-assertion\
-- Status: SUCCESS\
-- Description: "|_| *unsafe{ x.expose() } < 101"\
-in function modify
-
-VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/transmute/cell.rs b/tests/expected/function-contract/transmute/cell.rs
deleted file mode 100644
index 4616b090a5d6..000000000000
--- a/tests/expected/function-contract/transmute/cell.rs
+++ /dev/null
@@ -1,42 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
-
-/// This is a valid but not recommended alternative to havocing Cell
-/// Only done for test purposes
-
-/// ---------------------------------------------------
-///        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
-/// ---------------------------------------------------
-
-#[kani::requires(*unsafe{x.expose()} < 100)]
-#[kani::modifies(x.expose())]
-#[kani::ensures(|_| *unsafe{x.expose()} < 101)]
-fn modify(x: &Cell<u32>) {
-    // valid rust methodology for getting and setting value without breaking encapsulation
-    x.set(x.get() + 1)
-}
-
-#[kani::proof_for_contract(modify)]
-fn harness_for_modify() {
-    let x = Cell::new(kani::any());
-    modify(&x)
-}
diff --git a/tests/expected/function-contract/transmute/unsafecell.expected b/tests/expected/function-contract/transmute/unsafecell.expected
deleted file mode 100644
index da8fb418724e..000000000000
--- a/tests/expected/function-contract/transmute/unsafecell.expected
+++ /dev/null
@@ -1,6 +0,0 @@
-assertion\
-- Status: SUCCESS\
-- Description: "|_| *unsafe{ x.expose() } < 101"\
-in function modify
-
-VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/transmute/unsafecell.rs b/tests/expected/function-contract/transmute/unsafecell.rs
deleted file mode 100644
index 988e0312fea8..000000000000
--- a/tests/expected/function-contract/transmute/unsafecell.rs
+++ /dev/null
@@ -1,41 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
-
-/// This is a valid but not recommended alternative to havocing UnsafeCell
-/// Only done for test purposes
-
-/// ---------------------------------------------------
-///        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
-/// ---------------------------------------------------
-
-#[kani::requires(*unsafe{x.expose()} < 100)]
-#[kani::modifies(x.expose())]
-#[kani::ensures(|_| *unsafe{x.expose()} < 101)]
-fn modify(x: &UnsafeCell<u32>) {
-    unsafe { *x.get() += 1 }
-}
-
-#[kani::proof_for_contract(modify)]
-fn harness_for_modify() {
-    let x = UnsafeCell::new(kani::any());
-    modify(&x)
-}

From 13baa5ba339ae897cd0ff63264fc4c6ffc494aab Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <rms.felipe@gmail.com>
Date: Mon, 29 Jul 2024 23:27:16 -0400
Subject: [PATCH 20/32] Update
 tests/expected/function-contract/interior-mutability/api/unsafecell.rs

---
 .../function-contract/interior-mutability/api/unsafecell.rs     | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/expected/function-contract/interior-mutability/api/unsafecell.rs b/tests/expected/function-contract/interior-mutability/api/unsafecell.rs
index 18c9602a69c3..ae077130f21d 100644
--- a/tests/expected/function-contract/interior-mutability/api/unsafecell.rs
+++ b/tests/expected/function-contract/interior-mutability/api/unsafecell.rs
@@ -4,7 +4,7 @@
 
 use std::cell::UnsafeCell;
 
-/// This struct is contains UnsafeCell which can be mutated
+/// This struct contains UnsafeCell which can be mutated
 struct InteriorMutability {
     x: UnsafeCell<u32>,
 }

From 5feba8c76df38daa1141f056dffe79033be228f7 Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <rms.felipe@gmail.com>
Date: Mon, 29 Jul 2024 23:27:22 -0400
Subject: [PATCH 21/32] Update
 tests/expected/function-contract/interior-mutability/api/unsafecell.rs

---
 .../function-contract/interior-mutability/api/unsafecell.rs     | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/expected/function-contract/interior-mutability/api/unsafecell.rs b/tests/expected/function-contract/interior-mutability/api/unsafecell.rs
index ae077130f21d..8125e3e3c077 100644
--- a/tests/expected/function-contract/interior-mutability/api/unsafecell.rs
+++ b/tests/expected/function-contract/interior-mutability/api/unsafecell.rs
@@ -12,7 +12,7 @@ struct InteriorMutability {
 #[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
+/// `im` is an immutable reference with interior mutability
 fn modify(im: &InteriorMutability) {
     unsafe { *im.x.get() += 1 }
 }

From 7f84e89703fe53502bd5d9dab1427360a60fc3ef Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <rms.felipe@gmail.com>
Date: Mon, 29 Jul 2024 23:27:28 -0400
Subject: [PATCH 22/32] Update
 tests/expected/function-contract/interior-mutability/api/cell_stub.rs

---
 .../function-contract/interior-mutability/api/cell_stub.rs      | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/expected/function-contract/interior-mutability/api/cell_stub.rs b/tests/expected/function-contract/interior-mutability/api/cell_stub.rs
index 9e2b1ff52975..46c5570db9ac 100644
--- a/tests/expected/function-contract/interior-mutability/api/cell_stub.rs
+++ b/tests/expected/function-contract/interior-mutability/api/cell_stub.rs
@@ -3,7 +3,7 @@
 // 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
+/// This shows that we can generate `kani::any()` for Cell.
 use std::cell::Cell;
 
 /// This struct is contains Cell which can be mutated

From 882477cc67685c6961a7e5e1d6e56d9a83fe78ea Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <rms.felipe@gmail.com>
Date: Mon, 29 Jul 2024 23:27:34 -0400
Subject: [PATCH 23/32] Update
 tests/expected/function-contract/interior-mutability/api/cell_stub.rs

---
 .../function-contract/interior-mutability/api/cell_stub.rs      | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/expected/function-contract/interior-mutability/api/cell_stub.rs b/tests/expected/function-contract/interior-mutability/api/cell_stub.rs
index 46c5570db9ac..d01ca379655f 100644
--- a/tests/expected/function-contract/interior-mutability/api/cell_stub.rs
+++ b/tests/expected/function-contract/interior-mutability/api/cell_stub.rs
@@ -6,7 +6,7 @@
 /// This shows that we can generate `kani::any()` for Cell.
 use std::cell::Cell;
 
-/// This struct is contains Cell which can be mutated
+/// This struct contains Cell which can be mutated
 struct InteriorMutability {
     x: Cell<u32>,
 }

From 82c3e6fae3681aa91c30f215309e27770530156a Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <rms.felipe@gmail.com>
Date: Mon, 29 Jul 2024 23:27:39 -0400
Subject: [PATCH 24/32] Update
 tests/expected/function-contract/interior-mutability/api/cell.rs

---
 .../expected/function-contract/interior-mutability/api/cell.rs  | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/expected/function-contract/interior-mutability/api/cell.rs b/tests/expected/function-contract/interior-mutability/api/cell.rs
index c8dbf39bb159..13d081967ea7 100644
--- a/tests/expected/function-contract/interior-mutability/api/cell.rs
+++ b/tests/expected/function-contract/interior-mutability/api/cell.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-/// Mutating Cell via as_ptr in contracts
+/// Mutating Cell via `as_ptr` in contracts
 use std::cell::Cell;
 
 /// This struct is contains Cell which can be mutated

From 1e12172d3fdd1bd1a26b931f3e43a9c81b581f98 Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <rms.felipe@gmail.com>
Date: Mon, 29 Jul 2024 23:27:46 -0400
Subject: [PATCH 25/32] Update
 tests/expected/function-contract/interior-mutability/api/cell.rs

---
 .../expected/function-contract/interior-mutability/api/cell.rs  | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/expected/function-contract/interior-mutability/api/cell.rs b/tests/expected/function-contract/interior-mutability/api/cell.rs
index 13d081967ea7..671b6b206ef3 100644
--- a/tests/expected/function-contract/interior-mutability/api/cell.rs
+++ b/tests/expected/function-contract/interior-mutability/api/cell.rs
@@ -5,7 +5,7 @@
 /// Mutating Cell via `as_ptr` in contracts
 use std::cell::Cell;
 
-/// This struct is contains Cell which can be mutated
+/// This struct contains Cell which can be mutated
 struct InteriorMutability {
     x: Cell<u32>,
 }

From 42fd597b5550534d1ea7399b41546c07355377b6 Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <rms.felipe@gmail.com>
Date: Mon, 29 Jul 2024 23:27:53 -0400
Subject: [PATCH 26/32] Update
 tests/expected/function-contract/interior-mutability/whole-struct/cell.rs

---
 .../function-contract/interior-mutability/whole-struct/cell.rs  | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs
index a67aefa356fc..3de0b4a22520 100644
--- a/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs
@@ -5,7 +5,7 @@
 /// The objective of this test is to check the modification of a Cell used as interior mutability in an immutable struct
 use std::cell::Cell;
 
-/// This struct is contains Cell which can be mutated
+/// This struct contains Cell which can be mutated
 struct InteriorMutability {
     x: Cell<u32>,
 }

From 60b0d8ac9b9b8deb8fa541b86ca643781bf28b7f Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <rms.felipe@gmail.com>
Date: Mon, 29 Jul 2024 23:28:00 -0400
Subject: [PATCH 27/32] Update
 tests/expected/function-contract/interior-mutability/whole-struct/cell.rs

---
 .../function-contract/interior-mutability/whole-struct/cell.rs  | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs
index 3de0b4a22520..9f42f6fa1f6c 100644
--- a/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs
@@ -13,7 +13,7 @@ struct InteriorMutability {
 #[kani::requires(im.x.get() < 100)]
 #[kani::modifies(&im.x)]
 #[kani::ensures(|_| im.x.get() < 101)]
-///im is an immutable reference with interior mutability
+/// `im` is an immutable reference with interior mutability
 fn modify(im: &InteriorMutability) {
     im.x.set(im.x.get() + 1)
 }

From dbf938f1175430c1704b574b3a91ed3141ded0ab Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <rms.felipe@gmail.com>
Date: Mon, 29 Jul 2024 23:28:09 -0400
Subject: [PATCH 28/32] Update
 tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs

---
 .../interior-mutability/whole-struct/oncecell.rs                | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs
index 081de79adecf..6ca32251b60c 100644
--- a/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs
@@ -5,7 +5,7 @@
 /// The objective of this test is to check the modification of an OnceCell used as interior mutability in an immutable struct
 use std::cell::OnceCell;
 
-/// This struct is contains OnceCell which can be mutated
+/// This struct contains OnceCell which can be mutated
 struct InteriorMutability {
     x: OnceCell<u32>,
 }

From 065b554485419c10035caa139165bed3ba35cd51 Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <rms.felipe@gmail.com>
Date: Mon, 29 Jul 2024 23:28:16 -0400
Subject: [PATCH 29/32] Update
 tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs

---
 .../interior-mutability/whole-struct/refcell.rs                 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs
index df38d277f200..27a387d05c2b 100644
--- a/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs
@@ -5,7 +5,7 @@
 /// The objective of this test is to check the modification of a RefCell used as interior mutability in an immutable struct
 use std::cell::RefCell;
 
-/// This struct is contains Cell which can be mutated
+/// This struct contains Cell which can be mutated
 struct InteriorMutability {
     x: RefCell<u32>,
 }

From 19b4cbf69aea14de8dd6b82dcd8e79a4b9be45e4 Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <rms.felipe@gmail.com>
Date: Mon, 29 Jul 2024 23:28:21 -0400
Subject: [PATCH 30/32] Update
 tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs

---
 .../interior-mutability/whole-struct/refcell.rs                 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs
index 27a387d05c2b..1cce5e2364c3 100644
--- a/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs
@@ -13,7 +13,7 @@ struct InteriorMutability {
 #[kani::requires(unsafe{*im.x.as_ptr()} < 100)]
 #[kani::modifies(&im.x)]
 #[kani::ensures(|_| unsafe{*im.x.as_ptr()} < 101)]
-///im is an immutable reference with interior mutability
+/// `im` is an immutable reference with interior mutability
 fn modify(im: &InteriorMutability) {
     im.x.replace_with(|&mut old| old + 1);
 }

From aaf64edfe2341831e866e62570fc57c8d1732e62 Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <rms.felipe@gmail.com>
Date: Mon, 29 Jul 2024 23:28:27 -0400
Subject: [PATCH 31/32] Update
 tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs

---
 .../interior-mutability/whole-struct/unsafecell.rs              | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs
index 6cef4d62ce44..e93d8527c306 100644
--- a/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs
@@ -5,7 +5,7 @@
 /// The objective of this test is to check the modification of an UnsafeCell used as interior mutability in an immutable struct
 use std::cell::UnsafeCell;
 
-/// This struct is contains UnsafeCell which can be mutated
+/// This struct contains UnsafeCell which can be mutated
 struct InteriorMutability {
     x: UnsafeCell<u32>,
 }

From 172839f6e0b475c7e5ca43f643cd8702f5ce5079 Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <rms.felipe@gmail.com>
Date: Mon, 29 Jul 2024 23:28:32 -0400
Subject: [PATCH 32/32] Update
 tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs

---
 .../interior-mutability/whole-struct/unsafecell.rs              | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs
index e93d8527c306..6adb7b12c8b1 100644
--- a/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs
@@ -13,7 +13,7 @@ struct InteriorMutability {
 #[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
+/// `im` is an immutable reference with interior mutability
 fn modify(im: &InteriorMutability) {
     unsafe { *im.x.get() += 1 }
 }