chore: commit chagnes for rebase

Author: Stevengre

kmir/src/kmir/kdist/mir-semantics/rt/pointer-int.md

@@ -297,10 +297,9 @@ module RT-POINTER-INT
     requires WIDTH >Int 0
 
   syntax Int ::= #unsignedFromIntValue ( Int , Int , Bool ) [function, total]
-  rule #unsignedFromIntValue(VAL, _WIDTH, false) => VAL
-  rule #unsignedFromIntValue(VAL, _WIDTH, true) => VAL
+  rule #unsignedFromIntValue(VAL, _WIDTH, _SIGNED) => VAL
     requires VAL >=Int 0
-  rule #unsignedFromIntValue(VAL, WIDTH, true)
+  rule #unsignedFromIntValue(VAL, WIDTH, _SIGNED)
     => VAL +Int (1 <<Int WIDTH)
     requires VAL <Int 0
 

kmir/src/tests/integration/data/prove-rs/ptr-int-transmute.rs

@@ -1,15 +1,14 @@
-use std::cell::UnsafeCell;
 use std::mem::transmute;
 
 fn main() {
-    let cell = UnsafeCell::new(0_u8);
-    let ptr = cell.get();
+    let mut byte = 0_u8;
+    let ptr = &mut byte as *mut u8;
 
-    // Model code that leaks a raw pointer address to user space.
+    // Leak the raw pointer address as an integer.
     let leaked_addr = unsafe { transmute::<*mut u8, usize>(ptr) };
 
-    // …and then turns the address back into a pointer, assuming round-trip soundness.
+    // Turn it back into a pointer, assuming round-trip soundness.
     let restored_ptr = unsafe { transmute::<usize, *mut u8>(leaked_addr) };
 
-    // assert_eq!(ptr, restored_ptr);
+    assert_eq!(ptr, restored_ptr);
 }