port to rust 1.79.0

verus-lang · Oct 28, 2024 · 8071961 · 8071961
1 parent b6e766e
commit 8071961
Show file tree

Hide file tree

Showing 35 changed files with 560 additions and 228 deletions.
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
@@ -1,4 +1,4 @@
 [toolchain]
-channel = "1.76.0"
-# channel = "nightly-2023-09-29" # (not officially supported)
+channel = "1.79.0"
+# channel = "nightly-2023-09-29" # TODO update to match 1.79.0 (not officially supported)
 components = [ "rustc", "rust-std", "cargo", "rustfmt", "rustc-dev", "llvm-tools" ]
diff --git a/source/builtin/src/lib.rs b/source/builtin/src/lib.rs
@@ -145,9 +145,7 @@ pub fn opens_invariants_except<A>(_a: A) {
 #[cfg(verus_keep_ghost)]
 #[rustc_diagnostic_item = "verus::builtin::reveal_hide"]
 #[verifier::proof]
-pub fn reveal_hide_(_f: fn(), _n: u32) {
-    unimplemented!();
-}
+pub const fn reveal_hide_(_f: fn(), _n: u32) {}
 
 #[cfg(verus_keep_ghost)]
 #[rustc_diagnostic_item = "verus::builtin::reveal_hide_internal_path"]
@@ -348,14 +346,15 @@ impl<A> Ghost<A> {
     #[rustc_diagnostic_item = "verus::builtin::Ghost::view"]
     #[verifier::spec]
     pub fn view(self) -> A {
-        unimplemented!()
+        unsafe { core::mem::MaybeUninit::uninit().assume_init() }
     }
 
     #[cfg(verus_keep_ghost)]
     #[rustc_diagnostic_item = "verus::builtin::Ghost::new"]
     #[verifier::spec]
     #[verifier::external_body]
-    pub fn new(_a: A) -> Ghost<A> {
+    pub const fn new(_a: A) -> Ghost<A> {
+        core::mem::forget(_a);
         Ghost { phantom: PhantomData }
     }
 
@@ -382,7 +381,10 @@ impl<A> Ghost<A> {
     #[verifier::spec]
     #[verifier::external_body]
     pub fn borrow(&self) -> &A {
-        unimplemented!()
+        #[allow(deref_nullptr)]
+        unsafe {
+            &*(0 as *const A)
+        }
     }
 
     // note that because we return #[verifier::spec], not #[verifier::exec], we do not implement the BorrowMut trait
@@ -391,7 +393,10 @@ impl<A> Ghost<A> {
     #[verifier::proof]
     #[verifier::external]
     pub fn borrow_mut(#[verifier::proof] &mut self) -> &mut A {
-        unimplemented!()
+        #[allow(deref_nullptr)]
+        unsafe {
+            &mut *(0 as *mut A)
+        }
     }
 }
 
@@ -400,14 +405,15 @@ impl<A> Tracked<A> {
     #[rustc_diagnostic_item = "verus::builtin::Tracked::view"]
     #[verifier::spec]
     pub fn view(self) -> A {
-        unimplemented!()
+        unsafe { core::mem::MaybeUninit::uninit().assume_init() }
     }
 
     #[cfg(verus_keep_ghost)]
     #[rustc_diagnostic_item = "verus::builtin::Tracked::new"]
     #[verifier::proof]
     #[verifier::external_body]
-    pub fn new(#[verifier::proof] _a: A) -> Tracked<A> {
+    pub const fn new(#[verifier::proof] _a: A) -> Tracked<A> {
+        core::mem::forget(_a);
         Tracked { phantom: PhantomData }
     }
 
@@ -430,8 +436,8 @@ impl<A> Tracked<A> {
     #[verifier::proof]
     #[verifier::external_body]
     #[verifier::returns(proof)]
-    pub fn get(#[verifier::proof] self) -> A {
-        unimplemented!()
+    pub const fn get(#[verifier::proof] self) -> A {
+        unsafe { core::mem::MaybeUninit::uninit().assume_init() }
     }
 
     // note that because we return #[verifier::proof], not #[verifier::exec], we do not implement the Borrow trait
@@ -441,7 +447,10 @@ impl<A> Tracked<A> {
     #[verifier::external_body]
     #[verifier::returns(proof)]
     pub fn borrow(#[verifier::proof] &self) -> &A {
-        unimplemented!()
+        #[allow(deref_nullptr)]
+        unsafe {
+            &*(0 as *const A)
+        }
     }
 
     // note that because we return #[verifier::proof], not #[verifier::exec], we do not implement the BorrowMut trait
@@ -451,7 +460,10 @@ impl<A> Tracked<A> {
     #[verifier::external_body]
     #[verifier::returns(proof)]
     pub fn borrow_mut(#[verifier::proof] &mut self) -> &mut A {
-        unimplemented!()
+        #[allow(deref_nullptr)]
+        unsafe {
+            &mut *(0 as *mut A)
+        }
     }
 }
 
@@ -478,14 +490,16 @@ impl<A: Copy> Copy for Tracked<A> {}
 #[cfg(verus_keep_ghost)]
 #[rustc_diagnostic_item = "verus::builtin::ghost_exec"]
 #[verifier::external_body]
-pub fn ghost_exec<A>(#[verifier::spec] _a: A) -> Ghost<A> {
+pub const fn ghost_exec<A>(#[verifier::spec] _a: A) -> Ghost<A> {
+    core::mem::forget(_a);
     Ghost::assume_new()
 }
 
 #[cfg(verus_keep_ghost)]
 #[rustc_diagnostic_item = "verus::builtin::tracked_exec"]
 #[verifier::external_body]
-pub fn tracked_exec<A>(#[verifier::proof] _a: A) -> Tracked<A> {
+pub const fn tracked_exec<A>(#[verifier::proof] _a: A) -> Tracked<A> {
+    core::mem::forget(_a);
     Tracked::assume_new()
 }
 
@@ -1427,9 +1441,7 @@ pub fn infer_spec_for_loop_iter<A>(_: A, _print_hint: bool) -> Option<A> {
 #[cfg(verus_keep_ghost)]
 #[rustc_diagnostic_item = "verus::builtin::global_size_of"]
 #[verifier::spec]
-pub const fn global_size_of<T>(_bytes: usize) {
-    unimplemented!()
-}
+pub const fn global_size_of<T>(_bytes: usize) {}
 
 #[cfg(verus_keep_ghost)]
 #[rustc_diagnostic_item = "verus::builtin::inline_air_stmt"]