diff --git a/source/pervasive/layout.rs b/source/pervasive/layout.rs
new file mode 100644
index 0000000000..e5cfb9c779
--- /dev/null
+++ b/source/pervasive/layout.rs
@@ -0,0 +1,92 @@
+#![allow(unused_imports)]
+
+use builtin::*;
+use builtin_macros::*;
+use crate::prelude::*;
+
+verus!{
+
+// TODO add some means for Verus to calculate the size & alignment of types
+
+// TODO use a definition from a math library, once we have one.
+pub open spec fn is_power_2(n: int) -> bool
+    decreases n
+{
+    if n <= 0 {
+        false
+    } else if n == 1 {
+        true
+    } else {
+        n % 2 == 0 && is_power_2(n / 2)
+    }
+}
+
+/// Matches the conditions here: https://doc.rust-lang.org/stable/std/alloc/struct.Layout.html
+pub open spec fn valid_layout(size: usize, align: usize) -> bool {
+    is_power_2(align as int)
+      && size <= isize::MAX as int - (isize::MAX as int % align as int)
+}
+
+// The `V: Sized` bound is implicit in the below
+
+pub spec fn size_of<V>() -> nat;
+pub spec fn align_of<V>() -> nat;
+
+// Naturally, the size of any executable type is going to fit into a `usize`.
+// What I'm not sure of is whether it will be possible to "reason about" arbitrarily
+// big types _in ghost code_ without tripping one of rustc's checks.
+//
+// I think it could go like this:
+//   - Have some polymorphic code that constructs a giant tuple and proves false
+//   - Make sure the code doesn't get monomorphized by rustc
+//   - To export the 'false' fact from the polymorphic code without monomorphizing,
+//     use broadcast_forall.
+//
+// Therefore, we are NOT creating an axiom that `size_of` fits in usize.
+// However, we still give the guarantee that if you call `core::mem::size_of`
+// at runtime, then the resulting usize is correct.
+
+#[verifier(inline)]
+pub open spec fn size_of_as_usize<V>() -> usize
+    recommends size_of::<V>() as usize as int == size_of::<V>()
+{
+    size_of::<V>() as usize
+}
+
+#[verifier(inline)]
+pub open spec fn align_of_as_usize<V>() -> usize
+    recommends align_of::<V>() as usize as int == align_of::<V>()
+{
+    align_of::<V>() as usize
+}
+
+// This is marked as exec, again, in order to force `V` to be a real exec type.
+// Of course, it's still a no-op.
+
+#[verifier(external_body)]
+#[inline(always)]
+pub exec fn layout_for_type_is_valid<V>()
+    ensures
+        valid_layout(size_of::<V>() as usize, align_of::<V>() as usize),
+        size_of::<V>() as usize as nat == size_of::<V>(),
+        align_of::<V>() as usize as nat == align_of::<V>(),
+{
+}
+
+#[verifier::external_fn_specification]
+#[verifier::when_used_as_spec(size_of_as_usize)]
+pub fn ex_size_of<V>() -> (u: usize)
+    ensures u as nat == size_of::<V>()
+{
+    core::mem::size_of::<V>()
+}
+
+#[verifier::external_fn_specification]
+#[verifier::when_used_as_spec(align_of_as_usize)]
+pub fn ex_align_of<V>() -> (u: usize)
+    ensures u as nat == align_of::<V>()
+{
+    core::mem::align_of::<V>()
+}
+
+}
diff --git a/source/pervasive/ptr.rs b/source/pervasive/ptr.rs
index 5da411435e..f69f8d7adf 100644
--- a/source/pervasive/ptr.rs
+++ b/source/pervasive/ptr.rs
@@ -1,7 +1,9 @@
 #![allow(unused_imports)]
 
-use core::{marker, mem, mem::MaybeUninit};
 extern crate alloc;
+use alloc::alloc::Layout;
+use core::{marker, mem, mem::MaybeUninit};
+use alloc::alloc::Allocator;
 
 use builtin::*;
 use builtin_macros::*;
@@ -9,9 +11,11 @@ use crate::*;
 use crate::pervasive::*;
 use crate::modes::*;
 use crate::prelude::*;
+use crate::layout::*;
 
 verus!{
 
+
 /// `PPtr<V>` (which stands for "permissioned pointer")
 /// is a wrapper around a raw pointer to `V` on the heap.
 ///
@@ -116,13 +120,24 @@ verus!{
 //
 // However, int->ptr conversions ought to be allowed in the VERUS POINTER MODEL,
 // so I'm going with (2) here.
+//
+// TODO reconsider: Is this plan actually good? Exposing all pointers has the potential
+// to ruin optimizations. If the plan is bad, and we want to avoid the cost of
+// "expose-everywhere", we may need to actually track provenance as part
+// of the specification of PPtr.
+//
+// Perhaps what we could do is specify a low-level pointer library with
+// strict provenance rules + exposed pointers,
+// and then verify user libraries on top of that?
 
 // TODO implement: borrow_mut; figure out Drop, see if we can avoid leaking?
 
+// TODO just replace this with `*mut V`
+#[repr(C)]
 #[verifier(external_body)]
 #[verifier::accept_recursive_types(V)]
 pub struct PPtr<V> {
-    uptr: *mut MaybeUninit<V>,
+    uptr: *mut V,
 }
 
 // PPtr is always safe to Send/Sync. It's the PointsTo object where Send/Sync matters.
@@ -134,7 +149,7 @@ unsafe impl<T> Sync for PPtr<T> {}
 #[verifier(external)]
 unsafe impl<T> Send for PPtr<T> {}
 
-// TODO split up the "deallocation" permission and the "access" permission?
+// TODO some of functionality could have V: ?Sized
 
 /// A `tracked` ghost object that gives the user permission to dereference a pointer
 /// for reading or writing, or to free the memory at that pointer.
@@ -165,6 +180,49 @@ pub ghost struct PointsToData<V> {
     pub value: Option<V>,
 }
 
+// TODO add similiar height axioms for other ghost objects
+
+#[verifier(broadcast_forall)]
+#[verifier(external_body)]
+pub proof fn points_to_height_axiom<V>(points_to: PointsTo<V>)
+    ensures (#[trigger] height(points_to@)) < height(points_to)
+{
+    unimplemented!()
+}
+
+/// Points to uninitialized memory.
+
+#[verifier(external_body)]
+pub tracked struct PointsToRaw {
+    no_copy: NoCopy,
+}
+
+pub ghost struct PointsToRawData {
+    pub pptr: int,
+    pub size: nat,
+}
+
+#[verifier(external_body)]
+pub tracked struct Dealloc<#[verifier(strictly_positive)] V> {
+    phantom: marker::PhantomData<V>,
+    no_copy: NoCopy,
+}
+
+pub ghost struct DeallocData {
+    pub pptr: int,
+}
+
+#[verifier(external_body)]
+pub tracked struct DeallocRaw {
+    no_copy: NoCopy,
+}
+
+pub ghost struct DeallocRawData {
+    pub pptr: int,
+    pub size: nat,
+    pub align: nat,
+}
+
 impl<V> PointsTo<V> {
     pub spec fn view(self) -> PointsToData<V>;
 
@@ -188,8 +246,207 @@ impl<V> PointsTo<V> {
     }
 }
 
-impl<V> PPtr<V> {
+impl<V> PointsTo<V> {
+    #[verifier(external_body)]
+    pub proof fn into_raw(tracked self) -> (tracked points_to_raw: PointsToRaw)
+        requires
+            self@.value.is_None(),
+        ensures
+            points_to_raw@.pptr === self@.pptr,
+            points_to_raw@.size === size_of::<V>(),
+    {
+        unimplemented!();
+    }
+
+    #[verifier(external_body)]
+    pub proof fn borrow_raw(tracked &self) -> (tracked points_to_raw: &PointsToRaw)
+        requires
+            self@.value.is_None(),
+        ensures
+            points_to_raw@.pptr === self@.pptr,
+            points_to_raw@.size === size_of::<V>(),
+    {
+        unimplemented!();
+    }
+}
 
+impl PointsToRaw {
+    pub spec fn view(self) -> PointsToRawData;
+
+    #[verifier(external_body)]
+    pub proof fn is_nonnull(tracked &self)
+        ensures self@.pptr != 0,
+    {
+        unimplemented!();
+    }
+
+    #[verifier(external_body)]
+    pub proof fn is_in_bounds(tracked &self)
+        ensures (self@.pptr as usize) as int == self@.pptr,
+            ((self@.pptr + self@.size) as usize) as int == self@.pptr + self@.size
+    {
+        unimplemented!();
+    }
+
+    #[verifier(external_body)]
+    pub proof fn empty() -> (tracked points_to_raw: Self)
+    {
+        unimplemented!();
+    }
+
+    #[verifier(external_body)]
+    pub proof fn into_typed<V>(tracked self) -> (tracked points_to: PointsTo<V>)
+        requires
+            self@.size === size_of::<V>(),
+            self@.pptr % align_of::<V>() as int === 0,
+        ensures
+            points_to@.pptr === self@.pptr,
+            points_to@.value === None,
+    {
+        unimplemented!();
+    }
+
+    #[verifier(external_body)]
+    pub proof fn borrow_typed<V>(tracked &self) -> (tracked points_to: &PointsTo<V>)
+        requires
+            self@.size === size_of::<V>(),
+            self@.pptr % align_of::<V>() as int == 0,
+        ensures
+            points_to@.pptr === self@.pptr,
+            points_to@.value === None,
+    {
+        unimplemented!();
+    }
+
+    #[verifier(external_body)]
+    pub proof fn join(tracked self, tracked other: Self) -> (tracked joined: Self)
+        requires
+            self@.pptr + self@.size == other@.pptr,
+        ensures
+            joined@.pptr == self@.pptr,
+            joined@.size == self@.size + other@.size
+    {
+        unimplemented!();
+    }
+
+    #[verifier(external_body)]
+    pub proof fn borrow_join<'a>(tracked &'a self, tracked other: &'a Self) -> (tracked joined: &'a Self)
+        requires
+            self@.pptr + self@.size == other@.pptr,
+        ensures
+            joined@.pptr == self@.pptr,
+            joined@.size == self@.size + other@.size
+    {
+        unimplemented!();
+    }
+
+    #[verifier(external_body)]
+    pub proof fn split(tracked self, len1: int) -> (tracked res: (Self, Self))
+        requires
+            len1 <= self@.size
+        ensures
+            res.0@.pptr == self@.pptr,
+            res.0@.size == len1,
+            res.1@.pptr == self@.pptr + len1,
+            res.1@.size == self@.size - len1,
+    {
+        unimplemented!();
+    }
+            
+    #[verifier(external_body)]
+    pub proof fn borrow_split(tracked &self, len1: int) -> (tracked res: (&Self, &Self))
+        requires
+            len1 <= self@.size
+        ensures
+            res.0@.pptr == self@.pptr,
+            res.0@.size == len1,
+            res.1@.pptr == self@.pptr + len1,
+            res.1@.size == self@.size - len1,
+    {
+        unimplemented!();
+    }
+}
+
+impl<V> Dealloc<V> {
+    pub spec fn view(self) -> DeallocData;
+}
+
+impl<V> Dealloc<V> {
+    #[verifier(external_body)]
+    pub proof fn is_nonnull(tracked &self)
+        ensures self@.pptr != 0,
+    {
+        unimplemented!();
+    }
+
+    #[verifier(external_body)]
+    pub proof fn into_raw(tracked self) -> (tracked dealloc_raw: DeallocRaw)
+        ensures
+            dealloc_raw@.pptr === self@.pptr,
+            dealloc_raw@.size === size_of::<V>(),
+            dealloc_raw@.align === align_of::<V>(),
+    {
+        unimplemented!();
+    }
+
+    #[verifier(external_body)]
+    pub proof fn borrow_raw(tracked &self) -> (tracked dealloc_raw: &DeallocRaw)
+        ensures
+            dealloc_raw@.pptr === self@.pptr,
+            dealloc_raw@.size === size_of::<V>(),
+            dealloc_raw@.align === align_of::<V>(),
+    {
+        unimplemented!();
+    }
+}
+
+impl DeallocRaw {
+    pub spec fn view(self) -> DeallocRawData;
+
+    #[verifier(external_body)]
+    pub proof fn is_nonnull(tracked &self)
+        ensures self@.pptr != 0,
+    {
+        unimplemented!();
+    }
+
+    #[verifier(external_body)]
+    pub proof fn into_typed<V>(tracked self) -> (tracked dealloc: Dealloc<V>)
+        requires
+            self@.size === size_of::<V>(),
+            self@.align === align_of::<V>(),
+        ensures
+            dealloc@.pptr === self@.pptr,
+    {
+        unimplemented!();
+    }
+
+    #[verifier(external_body)]
+    pub proof fn borrow_typed<V>(tracked &self) -> (tracked dealloc: &Dealloc<V>)
+        requires
+            self@.size === size_of::<V>(),
+            self@.align === align_of::<V>(),
+        ensures
+            dealloc@.pptr === self@.pptr,
+    {
+        unimplemented!();
+    }
+}
+
+// TODO this currently doesn't work without `external`,
+// because of some temporary Verus trait limitations.
+// In the meantime, just use Copy.
+
+#[verifier(external)]
+impl<A> Clone for PPtr<A> {
+    fn clone(&self) -> Self {
+        PPtr { uptr: self.uptr }
+    }
+}
+
+impl<A> Copy for PPtr<A> { }
+
+impl<V> PPtr<V> {
     /// Cast a pointer to an integer.
 
     #[inline(always)]
@@ -222,7 +479,7 @@ impl<V> PPtr<V> {
     pub fn from_usize(u: usize) -> (p: Self)
         ensures p.id() == u as int,
     {
-        let uptr = u as *mut MaybeUninit<V>;
+        let uptr = u as *mut V;
         PPtr { uptr }
     }
 
@@ -230,30 +487,43 @@ impl<V> PPtr<V> {
 
     #[inline(always)]
     #[verifier(external_body)]
-    pub fn empty() -> (pt: (PPtr<V>, Tracked<PointsTo<V>>))
-        ensures pt.1@@ === (PointsToData{ pptr: pt.0.id(), value: Option::None }),
+    pub fn empty() -> (pt: (PPtr<V>, Tracked<PointsTo<V>>, Tracked<Dealloc<V>>))
+        ensures
+            pt.1@@ === (PointsToData{ pptr: pt.0.id(), value: None }),
+            pt.2@@ === (DeallocData{ pptr: pt.0.id() }),
         opens_invariants none
     {
+        // TODO abort on unwrap-failure
         let p = PPtr {
-            uptr: alloc::boxed::Box::leak(alloc::boxed::Box::new(MaybeUninit::uninit())).as_mut_ptr(),
+            uptr: alloc::alloc::Global.allocate(Layout::new::<V>()).unwrap().as_ptr() as *mut V,
         };
 
         // See explanation about exposing pointers, above
         let _exposed_addr = p.uptr as usize;
 
-        (p, Tracked::assume_new())
+        (p, Tracked::assume_new(), Tracked::assume_new())
     }
 
-    /// Clones the pointer.
-    /// TODO implement the `Clone` and `Copy` traits
-
     #[inline(always)]
     #[verifier(external_body)]
-    pub fn clone(&self) -> (pt: PPtr<V>)
-        ensures pt.id() === self.id(),
+    pub fn alloc(size: usize, align: usize) -> (pt: (PPtr<V>, Tracked<PointsToRaw>, Tracked<DeallocRaw>))
+        requires
+            valid_layout(size, align),
+        ensures
+            pt.1@@ === (PointsToRawData{ pptr: pt.0.id(), size: size as nat }),
+            pt.2@@ === (DeallocRawData{ pptr: pt.0.id(), size: size as nat, align: align as nat }),
+            pt.0.id() % align as int == 0,
         opens_invariants none
     {
-        PPtr { uptr: self.uptr }
+        let layout = unsafe { Layout::from_size_align_unchecked(size, align) };
+        let p = PPtr {
+            uptr: alloc::alloc::Global.allocate(layout).unwrap().as_ptr() as *mut V,
+        };
+
+        // See explanation about exposing pointers, above
+        let _exposed_addr = p.uptr as usize;
+
+        (p, Tracked::assume_new(), Tracked::assume_new())
     }
 
     /// Moves `v` into the location pointed to by the pointer `self`.
@@ -267,14 +537,17 @@ impl<V> PPtr<V> {
     pub fn put(&self, Tracked(perm): Tracked<&mut PointsTo<V>>, v: V)
         requires
             self.id() === old(perm)@.pptr,
-            old(perm)@.value === Option::None,
+            old(perm)@.value === None,
         ensures
             perm@.pptr === old(perm)@.pptr,
-            perm@.value === Option::Some(v),
+            perm@.value === Some(v),
         opens_invariants none
     {
+        // See explanation about exposing pointers, above
+        let ptr = self.uptr as usize as *mut V;
+
         unsafe {
-            *(self.uptr) = MaybeUninit::new(v);
+            *ptr = v;
         }
     }
 
@@ -294,14 +567,15 @@ impl<V> PPtr<V> {
             old(perm)@.value.is_Some(),
         ensures
             perm@.pptr === old(perm)@.pptr,
-            perm@.value === Option::None,
+            perm@.value === None,
             v === old(perm)@.value.get_Some_0(),
         opens_invariants none
     {
+        // See explanation about exposing pointers, above
+        let ptr = self.uptr as usize as *mut V;
+
         unsafe {
-            let mut m = MaybeUninit::uninit();
-            mem::swap(&mut m, &mut *self.uptr);
-            m.assume_init()
+            core::ptr::read(ptr)
         }
     }
 
@@ -316,14 +590,17 @@ impl<V> PPtr<V> {
             old(perm)@.value.is_Some(),
         ensures
             perm@.pptr === old(perm)@.pptr,
-            perm@.value === Option::Some(in_v),
+            perm@.value === Some(in_v),
             out_v === old(perm)@.value.get_Some_0(),
         opens_invariants none
     {
+        // See explanation about exposing pointers, above
+        let ptr = self.uptr as usize as *mut V;
+
         unsafe {
-            let mut m = MaybeUninit::new(in_v);
-            mem::swap(&mut m, &mut *self.uptr);
-            m.assume_init()
+            let mut m = in_v;
+            mem::swap(&mut m, &mut *ptr);
+            m
         }
     }
 
@@ -341,8 +618,11 @@ impl<V> PPtr<V> {
         ensures *v === perm@.value.get_Some_0(),
         opens_invariants none
     {
+        // See explanation about exposing pointers, above
+        let ptr = self.uptr as usize as *mut V;
+
         unsafe {
-            (*self.uptr).assume_init_ref()
+            &*ptr
         }
     }
 
@@ -354,14 +634,41 @@ impl<V> PPtr<V> {
 
     #[inline(always)]
     #[verifier(external_body)]
-    pub fn dispose(&self, Tracked(perm): Tracked<PointsTo<V>>)
+    pub fn dispose(&self, Tracked(perm): Tracked<PointsTo<V>>, Tracked(dealloc): Tracked<Dealloc<V>>)
         requires
             self.id() === perm@.pptr,
-            perm@.value === Option::None,
+            perm@.value === None,
+            perm@.pptr == dealloc@.pptr,
+        opens_invariants none
+    {
+        unsafe {
+            let nn = core::ptr::NonNull::new_unchecked(self.uptr as *mut u8);
+            alloc::alloc::Global.deallocate(nn, alloc::alloc::Layout::for_value(&*self.uptr));
+        }
+    }
+
+    #[inline(always)]
+    #[verifier(external_body)]
+    pub fn dealloc(&self,
+        size: usize,
+        align: usize,
+        Tracked(perm): Tracked<PointsToRaw>,
+        Tracked(dealloc): Tracked<DeallocRaw>
+    )
+        requires
+            perm@.pptr === self.id(),
+            perm@.size === size as nat,
+            dealloc@.pptr === self.id(),
+            dealloc@.size === size as nat,
+            dealloc@.align === align as nat,
         opens_invariants none
     {
         unsafe {
-            alloc::alloc::dealloc(self.uptr as *mut u8, alloc::alloc::Layout::for_value(&*self.uptr));
+            // Since we have the Dealloc object, we know this is a valid layout
+            // and that it's safe to call 'deallocate'
+            let layout = Layout::from_size_align_unchecked(size, align);
+            let nn = core::ptr::NonNull::new_unchecked(self.uptr as *mut u8);
+            alloc::alloc::Global.deallocate(nn, alloc::alloc::Layout::for_value(&*self.uptr));
         }
     }
 
@@ -375,9 +682,10 @@ impl<V> PPtr<V> {
     /// access to the memory by freeing it.
 
     #[inline(always)]
-    pub fn into_inner(self, Tracked(perm): Tracked<PointsTo<V>>) -> (v: V)
+    pub fn into_inner(self, Tracked(perm): Tracked<PointsTo<V>>, Tracked(dealloc): Tracked<Dealloc<V>>) -> (v: V)
         requires
             self.id() === perm@.pptr,
+            perm@.pptr == dealloc@.pptr,
             perm@.value.is_Some(),
         ensures
             v === perm@.value.get_Some_0(),
@@ -385,7 +693,7 @@ impl<V> PPtr<V> {
     {
         let tracked mut perm = perm;
         let v = self.take(Tracked(&mut perm));
-        self.dispose(Tracked(perm));
+        self.dispose(Tracked(perm), Tracked(dealloc));
         v
     }
 
@@ -393,13 +701,14 @@ impl<V> PPtr<V> {
     /// with the given value `v`.
 
     #[inline(always)]
-    pub fn new(v: V) -> (pt: (PPtr<V>, Tracked<PointsTo<V>>))
+    pub fn new(v: V) -> (pt: (PPtr<V>, Tracked<PointsTo<V>>, Tracked<Dealloc<V>>))
         ensures
-            (pt.1@@ === PointsToData{ pptr: pt.0.id(), value: Option::Some(v) }),
+            (pt.1@@ === PointsToData{ pptr: pt.0.id(), value: Some(v) }),
+            (pt.2@@ === DeallocData{ pptr: pt.0.id() }),
     {
-        let (p, Tracked(mut t)) = Self::empty();
+        let (p, Tracked(mut t), Tracked(d)) = Self::empty();
         p.put(Tracked(&mut t), v);
-        (p, Tracked(t))
+        (p, Tracked(t), Tracked(d))
     }
 }
 
diff --git a/source/pervasive/vstd.rs b/source/pervasive/vstd.rs
index 599627ceee..f64e62f0f6 100644
--- a/source/pervasive/vstd.rs
+++ b/source/pervasive/vstd.rs
@@ -22,6 +22,7 @@ pub mod invariant;
 pub mod atomic;
 pub mod atomic_ghost;
 pub mod modes;
+pub mod layout;
 pub mod multiset;
 pub mod function;
 pub mod state_machine_internal;
diff --git a/source/rust_verify/example/doubly_linked_xor.rs b/source/rust_verify/example/doubly_linked_xor.rs
index a8e7e61077..4f392a6b28 100644
--- a/source/rust_verify/example/doubly_linked_xor.rs
+++ b/source/rust_verify/example/doubly_linked_xor.rs
@@ -30,9 +30,11 @@ struct Node<V> {
 // Contains head pointer, tail pointer
 // and in ghost code, tracks all the pointers and all the permissions to access the nodes
 
+type MemPerms<V> = (PointsTo<Node<V>>, Dealloc<Node<V>>);
+
 struct DListXor<V> {
     ptrs: Ghost<Seq<PPtr<Node<V>>>>,
-    perms: Tracked<Map<nat, PointsTo<Node<V>>>>,
+    perms: Tracked<Map<nat, MemPerms<V>>>,
 
     head: u64,
     tail: u64,
@@ -67,11 +69,12 @@ impl<V> DListXor<V> {
         recommends i < self.ptrs@.len()
     {
         &&& self.perms@.dom().contains(i)
-        &&& self.perms@[i].view().pptr == self.ptrs@[i as int].id()
+        &&& self.perms@[i].0.view().pptr == self.ptrs@[i as int].id()
+        &&& self.perms@[i].1.view().pptr == self.ptrs@[i as int].id()
         &&& 0 < self.ptrs@[i as int].id()
         &&& self.ptrs@[i as int].id() < 0x10000000000000000
-        &&& self.perms@[i].view().value.is_Some()
-        &&& self.perms@[i].view().value.get_Some_0().xored == (
+        &&& self.perms@[i].0.view().value.is_Some()
+        &&& self.perms@[i].0.view().value.get_Some_0().xored == (
             self.prev_of(i) ^ self.next_of(i)
         )
     }
@@ -102,7 +105,7 @@ impl<V> DListXor<V> {
     {
 
         Seq::<V>::new(self.ptrs@.len(), |i: int| {
-            self.perms@[i as nat]@.value.get_Some_0().v
+            self.perms@[i as nat].0@.value.get_Some_0().v
         })
     }
 
@@ -127,15 +130,14 @@ impl<V> DListXor<V> {
             self.wf(),
             self@ == old(self)@.push(v),
     {
-        let (ptr, perm) = PPtr::new(
+        let (ptr, Tracked(perm), Tracked(dealloc)) = PPtr::new(
             Node::<V> { xored: 0, v }
         );
         proof {
             self.ptrs@ = self.ptrs@.push(ptr);
-            let tracked perm = perm.get();
             (&perm).is_nonnull();
-            (self.perms.borrow_mut())
-                .tracked_insert((self.ptrs@.len() - 1) as nat, perm);
+            self.perms.borrow_mut()
+                .tracked_insert((self.ptrs@.len() - 1) as nat, (perm, dealloc));
         }
 
         self.tail = ptr.to_usize() as u64;
@@ -169,17 +171,17 @@ impl<V> DListXor<V> {
             let tail_ptr_u64 = self.tail;
             proof { lemma_usize_u64(tail_ptr_u64); }
             let tail_ptr = PPtr::<Node<V>>::from_usize(tail_ptr_u64 as usize);
-            let tracked mut tail_perm: PointsTo<Node<V>> =
-                (self.perms.borrow_mut()).tracked_remove((self.ptrs@.len() - 1) as nat);
+            let tracked (mut tail_perm, de): MemPerms<V> =
+                self.perms.borrow_mut().tracked_remove((self.ptrs@.len() - 1) as nat);
             let mut tail_node = tail_ptr.take(Tracked(&mut tail_perm));
             let second_to_last_ptr = tail_node.xored;
 
-            let (ptr, perm) = PPtr::new(
+            let (ptr, Tracked(perm), Tracked(dealloc)) = PPtr::new(
                 Node::<V> { xored: tail_ptr_u64, v }
             );
 
             proof {
-                (perm.borrow()).is_nonnull();
+                perm.is_nonnull();
             }
 
             let new_ptr_u64 = ptr.to_usize() as u64;
@@ -187,10 +189,10 @@ impl<V> DListXor<V> {
             tail_node.xored = second_to_last_ptr ^ new_ptr_u64;
             tail_ptr.put(Tracked(&mut tail_perm), tail_node);
             proof {
-                (self.perms.borrow_mut())
-                    .tracked_insert((self.ptrs@.len() - 1) as nat, tail_perm);
-                (self.perms.borrow_mut())
-                    .tracked_insert(self.ptrs@.len(), (perm).get());
+                self.perms.borrow_mut()
+                    .tracked_insert((self.ptrs@.len() - 1) as nat, (tail_perm, de));
+                self.perms.borrow_mut()
+                    .tracked_insert(self.ptrs@.len(), (perm, dealloc));
                 self.ptrs@ = self.ptrs@.push(ptr);
             }
             self.tail = new_ptr_u64;
@@ -240,10 +242,9 @@ impl<V> DListXor<V> {
         let last_u64 = self.tail;
         proof { lemma_usize_u64(last_u64); }
         let last_ptr = PPtr::<Node<V>>::from_usize(last_u64 as usize);
-        let last_perm: Tracked<PointsTo<Node<V>>> = Tracked(
-            (self.perms.borrow_mut()).tracked_remove((self.ptrs@.len() - 1) as nat)
-        );
-        let last_node = last_ptr.into_inner(last_perm);
+        let tracked last_perm: MemPerms<V> =
+            self.perms.borrow_mut().tracked_remove((self.ptrs@.len() - 1) as nat);
+        let last_node = last_ptr.into_inner(Tracked(last_perm.0), Tracked(last_perm.1));
 
         let penult_u64 = last_node.xored;
         let v = last_node.v;
@@ -279,8 +280,8 @@ impl<V> DListXor<V> {
                 lemma_usize_u64(penult_u64);
             }
             let penult_ptr = PPtr::<Node<V>>::from_usize(penult_u64 as usize);
-            let tracked mut penult_perm =
-                (self.perms.borrow_mut()).tracked_remove((self.ptrs@.len() - 2) as nat);
+            let tracked (mut penult_perm, de) =
+                self.perms.borrow_mut().tracked_remove((self.ptrs@.len() - 2) as nat);
             let mut penult_node = penult_ptr.take(Tracked(&mut penult_perm));
             let t: Ghost<u64> = Ghost(self.prev_of((self.ptrs@.len() - 2) as nat));
             assert((t@ ^ last_u64) ^ last_u64 == t@ ^ 0) by(bit_vector);
@@ -291,8 +292,8 @@ impl<V> DListXor<V> {
 
             penult_ptr.put(Tracked(&mut penult_perm), penult_node);
             proof {
-                (self.perms.borrow_mut())
-                    .tracked_insert((self.ptrs@.len() - 2) as nat, penult_perm);
+                self.perms.borrow_mut()
+                    .tracked_insert((self.ptrs@.len() - 2) as nat, (penult_perm, de));
             }
         }
 
@@ -349,10 +350,9 @@ impl<V> DListXor<V> {
         let first_u64 = self.head;
         proof { lemma_usize_u64(first_u64); }
         let first_ptr = PPtr::<Node<V>>::from_usize(first_u64 as usize);
-        let first_perm: Tracked<PointsTo<Node<V>>> = Tracked(
-            (self.perms.borrow_mut()).tracked_remove(0)
-        );
-        let first_node = first_ptr.into_inner(first_perm);
+        let tracked first_perm: MemPerms<V> = 
+            self.perms.borrow_mut().tracked_remove(0);
+        let first_node = first_ptr.into_inner(Tracked(first_perm.0), Tracked(first_perm.1));
 
         let second_u64 = first_node.xored;
         let v = first_node.v;
@@ -388,7 +388,7 @@ impl<V> DListXor<V> {
                 lemma_usize_u64(second_u64);
             }
             let second_ptr = PPtr::<Node<V>>::from_usize(second_u64 as usize);
-            let tracked mut second_perm = (self.perms.borrow_mut()).tracked_remove(1);
+            let tracked (mut second_perm, de) = (self.perms.borrow_mut()).tracked_remove(1);
             let mut second_node = second_ptr.take(Tracked(&mut second_perm));
             let t: Ghost<u64> = Ghost(self.next_of(1));
             assert((first_u64 ^ t@) ^ first_u64 == 0 ^ t@) by(bit_vector);
@@ -399,8 +399,8 @@ impl<V> DListXor<V> {
 
             second_ptr.put(Tracked(&mut second_perm), second_node);
             proof {
-                (self.perms.borrow_mut())
-                    .tracked_insert(1, second_perm);
+                self.perms.borrow_mut()
+                    .tracked_insert(1, (second_perm, de));
 
                 assert forall |j: nat| 1 <= j < old(self)@.len() implies
                     self.perms@.dom().contains(j)
@@ -469,17 +469,17 @@ impl<V> DListXor<V> {
             let head_ptr_u64 = self.head;
             proof { lemma_usize_u64(head_ptr_u64); }
             let head_ptr = PPtr::<Node<V>>::from_usize(head_ptr_u64 as usize);
-            let tracked mut head_perm: PointsTo<Node<V>> =
+            let tracked (mut head_perm, de): MemPerms<V> =
                 (self.perms.borrow_mut()).tracked_remove(0);
             let mut head_node = head_ptr.take(Tracked(&mut head_perm));
             let second_ptr = head_node.xored;
 
-            let (ptr, perm) = PPtr::new(
+            let (ptr, Tracked(perm), Tracked(dealloc)) = PPtr::new(
                 Node::<V> { xored: head_ptr_u64, v }
             );
 
             proof {
-                (perm.borrow()).is_nonnull();
+                perm.is_nonnull();
             }
 
             let new_ptr_u64 = ptr.to_usize() as u64;
@@ -487,22 +487,22 @@ impl<V> DListXor<V> {
             head_node.xored = new_ptr_u64 ^ second_ptr;
             head_ptr.put(Tracked(&mut head_perm), head_node);
             proof {
-                (self.perms.borrow_mut())
-                    .tracked_insert(0, head_perm);
+                self.perms.borrow_mut()
+                    .tracked_insert(0, (head_perm, de));
 
                 assert forall |j: nat| 0 <= j < old(self)@.len() implies
                     self.perms@.dom().contains(j)
                 by { assert(old(self).wf_perm(j)); }
 
-                (self.perms.borrow_mut()).tracked_map_keys_in_place(
+                self.perms.borrow_mut().tracked_map_keys_in_place(
                     Map::<nat, nat>::new(
                         |j: nat| 1 <= j <= old(self)@.len(),
                         |j: nat| (j - 1) as nat,
                     )
                 );
 
-                (self.perms.borrow_mut())
-                    .tracked_insert(0, (perm).get());
+                self.perms.borrow_mut()
+                    .tracked_insert(0, (perm, dealloc));
                 self.ptrs@ = seq![ptr].add(self.ptrs@);
             }
             self.head = new_ptr_u64;
@@ -522,9 +522,9 @@ impl<V> DListXor<V> {
                 //    self.prev_of(i) ^ self.next_of(i)
                 //));
 
-                assert(self.perms@.index(1)@.value.get_Some_0().xored == new_ptr_u64 ^ second_ptr);
-                assert(self.perms@.index(0)@.value.get_Some_0().xored == head_ptr_u64);
-                assert(self.perms@.index(1)@.pptr == head_ptr_u64 as int);
+                assert(self.perms@.index(1).0@.value.get_Some_0().xored == new_ptr_u64 ^ second_ptr);
+                assert(self.perms@.index(0).0@.value.get_Some_0().xored == head_ptr_u64);
+                assert(self.perms@.index(1).0@.pptr == head_ptr_u64 as int);
 
                 assert(self.wf_perm(1));
                 assert(self.wf_perm(0));
diff --git a/source/rust_verify/example/rfmig_script.rs b/source/rust_verify/example/rfmig_script.rs
index 7e8e6dd6d6..381422f972 100644
--- a/source/rust_verify/example/rfmig_script.rs
+++ b/source/rust_verify/example/rfmig_script.rs
@@ -210,7 +210,7 @@ fn start_thread(counter: PPtr<u64>, Tracked(perm): Tracked<PointsTo<u64>>)
     requires
         counter.id() == perm@.pptr, perm@.value === None,
 {
-    send_pointer(counter.clone());
+    send_pointer(counter);
 
     let tracked mut perm: PointsTo<u64> = perm;
 
diff --git a/source/rust_verify/example/state_machines/tutorial/rc.rs b/source/rust_verify/example/state_machines/tutorial/rc.rs
index 1d0e0063b0..6d473baa8b 100644
--- a/source/rust_verify/example/state_machines/tutorial/rc.rs
+++ b/source/rust_verify/example/state_machines/tutorial/rc.rs
@@ -198,13 +198,15 @@ struct InnerRc<S> {
     pub s: S,
 }
 
+type MemPerms<S> = (ptr::PointsTo<InnerRc<S>>, ptr::Dealloc<InnerRc<S>>);
+
 tracked struct GhostStuff<S> {
     pub tracked rc_perm: cell::PointsTo<u64>,
-    pub tracked rc_token: RefCounter::counter<ptr::PointsTo<InnerRc<S>>>,
+    pub tracked rc_token: RefCounter::counter<MemPerms<S>>,
 }
 
 impl<S> GhostStuff<S> {
-    pub open spec fn wf(self, inst: RefCounter::Instance<ptr::PointsTo<InnerRc<S>>>, cell: PCell<u64>) -> bool {
+    pub open spec fn wf(self, inst: RefCounter::Instance<MemPerms<S>>, cell: PCell<u64>) -> bool {
         &&& self.rc_perm@.pcell == cell.id()
         &&& self.rc_token@.instance == inst
         &&& self.rc_perm@.value.is_Some()
@@ -220,9 +222,9 @@ impl<S> InnerRc<S> {
 
 struct_with_invariants!{
     struct MyRc<S> {
-        pub inst: Tracked< RefCounter::Instance<ptr::PointsTo<InnerRc<S>>> >,
+        pub inst: Tracked< RefCounter::Instance<MemPerms<S>> >,
         pub inv: Tracked< Duplicable<LocalInvariant<_, GhostStuff<S>, _>> >,
-        pub reader: Tracked< RefCounter::reader<ptr::PointsTo<InnerRc<S>>> >,
+        pub reader: Tracked< RefCounter::reader<MemPerms<S>> >,
 
         pub ptr: PPtr<InnerRc<S>>,
 
@@ -231,12 +233,14 @@ struct_with_invariants!{
 
     spec fn wf(self) -> bool {
         predicate {
-            &&& self.reader@@.key@.pptr == self.ptr.id()
+            &&& self.reader@@.key.0@.pptr == self.ptr.id()
+            &&& self.reader@@.key.1@.pptr == self.ptr.id()
+
             &&& self.reader@@.instance == self.inst@
             &&& self.reader@@.count == 1
-            &&& self.reader@@.key@.value.is_Some()
+            &&& self.reader@@.key.0@.value.is_Some()
             &&& self.inv@.wf()
-            &&& self.reader@@.key@.value.get_Some_0().rc_cell == self.rc_cell
+            &&& self.reader@@.key.0@.value.get_Some_0().rc_cell == self.rc_cell
         }
 
         invariant on inv with (inst, rc_cell)
@@ -250,7 +254,7 @@ struct_with_invariants!{
 
 impl<S> MyRc<S> {
     spec fn view(self) -> S {
-        self.reader@@.key@.value.get_Some_0().s
+        self.reader@@.key.0@.value.get_Some_0().s
     }
 
     fn new(s: S) -> (rc: Self)
@@ -258,34 +262,20 @@ impl<S> MyRc<S> {
             rc.wf(),
             rc@ == s,
     {
-
         let (rc_cell, Tracked(rc_perm)) = PCell::new(1);
         let inner_rc = InnerRc::<S> { rc_cell, s };
 
-        let (ptr, Tracked(ptr_perm)) = PPtr::new(inner_rc);
+        let (ptr, Tracked(ptr_perm), Tracked(dealloc_perm)) = PPtr::new(inner_rc);
 
-        let tracked inst;
-        let tracked reader;
-        let tracked inv;
-        let tracked g;
-        proof {
-            let tracked (Tracked(inst0), Tracked(mut rc_token), _) = RefCounter::Instance::initialize_empty(Option::None);
-            inst = inst0;
+        let tracked (Tracked(inst), Tracked(mut rc_token), _) = RefCounter::Instance::initialize_empty(Option::None);
+        let tracked reader = inst.do_deposit((ptr_perm, dealloc_perm), &mut rc_token, (ptr_perm, dealloc_perm));
+        let tracked g = GhostStuff::<S> { rc_perm, rc_token };
 
-            let tracked reader0 = inst.do_deposit(ptr_perm, &mut rc_token, ptr_perm);
-            g = GhostStuff::<S> { rc_perm, rc_token };
-            reader = reader0;
-        }
         let tr_inst = Tracked(inst);
         let gh_cell = Ghost(rc_cell);
 
-        proof {
-            let tracked inv0 = LocalInvariant::new(
-                (tr_inst, gh_cell), g, 0);
-            let tracked inv0 = Duplicable::new(inv0);
-
-            inv = inv0;
-        }
+        let tracked inv = LocalInvariant::new((tr_inst, gh_cell), g, 0);
+        let tracked inv = Duplicable::new(inv);
 
         MyRc {
             inst: tr_inst, inv: Tracked(inv), reader: Tracked(reader),
@@ -301,7 +291,7 @@ impl<S> MyRc<S> {
         let tracked inst = self.inst.borrow();
         let tracked reader = self.reader.borrow();
         let tracked perm = inst.reader_guard(reader@.key, &reader);
-        &self.ptr.borrow(Tracked(perm)).s
+        &self.ptr.borrow(Tracked(&perm.0)).s
     }
 
     fn clone(&self) -> (s: Self)
@@ -312,7 +302,7 @@ impl<S> MyRc<S> {
         let tracked reader = self.reader.borrow();
 
         let tracked perm = inst.reader_guard(reader@.key, &reader);
-        let inner_rc_ref = self.ptr.borrow(Tracked(perm));
+        let inner_rc_ref = self.ptr.borrow(Tracked(&perm.0));
 
         let tracked new_reader;
         open_local_invariant!(self.inv.borrow().borrow() => g => {
@@ -339,7 +329,7 @@ impl<S> MyRc<S> {
             inst: Tracked(self.inst.borrow().clone()),
             inv: Tracked(self.inv.borrow().clone()),
             reader: Tracked(new_reader),
-            ptr: self.ptr.clone(),
+            ptr: self.ptr,
             rc_cell: Ghost(self.rc_cell@),
         }
     }
@@ -353,7 +343,7 @@ impl<S> MyRc<S> {
             reader@.key,
             &reader);
 
-        let inner_rc_ref = &ptr.borrow(Tracked(perm));
+        let inner_rc_ref = &ptr.borrow(Tracked(&perm.0));
 
         open_local_invariant!(inv.borrow() => g => {
             let tracked GhostStuff { rc_perm: mut rc_perm, rc_token: mut rc_token } = g;
@@ -370,7 +360,7 @@ impl<S> MyRc<S> {
                         reader);
                 }
             } else {
-                let tracked mut inner_rc_perm = inst.dec_to_zero(
+                let tracked (mut inner_rc_perm, inner_rc_dealloc) = inst.dec_to_zero(
                     reader.view().key,
                     &mut rc_token,
                     reader);
@@ -383,7 +373,7 @@ impl<S> MyRc<S> {
                 let count = count - 1;
                 inner_rc.rc_cell.put(Tracked(&mut rc_perm), count);
 
-                ptr.dispose(Tracked(inner_rc_perm));
+                ptr.dispose(Tracked(inner_rc_perm), Tracked(inner_rc_dealloc));
             }
 
             proof { g = GhostStuff { rc_perm, rc_token }; }
diff --git a/source/rust_verify/example/verified_vec.rs b/source/rust_verify/example/verified_vec.rs
new file mode 100644
index 0000000000..b24a02aad8
--- /dev/null
+++ b/source/rust_verify/example/verified_vec.rs
@@ -0,0 +1,173 @@
+#![allow(unused_imports)]
+
+use builtin::*;
+use builtin_macros::*;
+use vstd::*;
+use vstd::modes::*;
+use vstd::ptr::*;
+use vstd::prelude::*;
+use vstd::layout::*;
+
+verus!{
+
+struct Vector<V> {
+    pub ptr: PPtr<V>,
+    pub len: usize,
+    pub capacity: usize,
+
+    pub elems: Tracked<Map<nat, PointsTo<V>>>,
+    pub rest: Tracked<PointsToRaw>,
+    pub dealloc: Tracked<DeallocRaw>,
+}
+
+impl<V: SizeOf> Vector<V> {
+    pub closed spec fn well_formed(&self) -> bool {
+        &&& self.len <= self.capacity
+        &&& (forall |i: nat| 0 <= i < self.len ==>
+            self.elems@.dom().contains(i))
+        &&& (forall |i: nat| 0 <= i < self.len ==>
+            (#[trigger] self.elems@.index(i))@.pptr
+              == self.ptr.id() + i as int * size_of::<V>())
+        &&& (forall |i: nat| 0 <= i < self.len ==>
+            (#[trigger] self.elems@.index(i))@.value.is_Some())
+        &&& self.rest@@.pptr == self.ptr.id() + self.len * size_of::<V>()
+        &&& self.rest@@.size == (self.capacity - self.len) * size_of::<V>()
+        &&& self.dealloc@@.pptr == self.ptr.id()
+        &&& self.dealloc@@.size == self.capacity * size_of::<V>()
+        &&& self.dealloc@@.align == align_of::<V>()
+    }
+
+    pub closed spec fn view(&self) -> Seq<V> {
+        Seq::new(
+          self.len as nat,
+          |i: int| self.elems@.index(i as nat)@.value.get_Some_0(),
+        )
+    }
+
+    pub fn empty() -> (vec: Self)
+        ensures vec.well_formed(),
+    {
+        proof {
+            layout_for_type_is_valid::<V>();
+        }
+        let (p, Tracked(points_to), Tracked(dealloc)) =
+            PPtr::<V>::alloc(0, get_align_of::<V>());
+
+        Vector {
+            ptr: p,
+            len: 0,
+            capacity: 0,
+            elems: Tracked(Map::tracked_empty()),
+            rest: Tracked(points_to),
+            dealloc: Tracked(dealloc),
+        }
+    }
+
+    pub fn index(&self, i: usize) -> (elem: &V)
+        requires
+            self.well_formed(),
+            0 <= i < self@.len(),
+        ensures
+            *elem === self@.index(i as int),
+    {
+        let ptr_usize = self.ptr.to_usize();
+
+        assume(
+            (i as int * size_of::<V>()) as usize as int
+            == (i as int * size_of::<V>()));
+        assume(
+            (ptr_usize as int + i as int * size_of::<V>()) as usize as int
+            == (ptr_usize as int + i as int * size_of::<V>()));
+
+        let elem_ptr_usize = ptr_usize + i * get_size_of::<V>();
+        let elem_ptr = PPtr::<V>::from_usize(elem_ptr_usize);
+
+        let tracked perm = self.elems.borrow().tracked_borrow(i as nat);
+
+        elem_ptr.borrow(Tracked(perm))
+    }
+
+    pub fn resize(&mut self, new_capacity: usize)
+        requires
+            old(self).well_formed(),
+            old(self).len <= new_capacity,
+        ensures
+            self.well_formed(),
+            old(self)@ === self@,
+            self.capacity === new_capacity,
+    {
+        // TODO implement
+        assume(false);
+    }
+
+    pub fn push(&mut self, v: V)
+        requires
+            old(self).well_formed(),
+        ensures
+            self@ === old(self)@.push(v)
+    {
+        if self.len == self.capacity {
+            assume((self.capacity as int * 2) as usize as int 
+                == (self.capacity as int * 2));
+            let new_cap = if self.capacity == 0 { 2 } else { self.capacity * 2 };
+            self.resize(new_cap);
+
+            assert((if self.capacity == 0 { 2 } else { self.capacity * 2 }) > self.capacity) by (nonlinear_arith);
+            assert(new_cap > old(self).capacity);
+            assert(self@.len() == old(self)@.len());
+            assert(self.len == old(self).len);
+            assert(self.len < self.capacity);
+        }
+        assert(self.len < self.capacity);
+
+        let tracked mut points_to;
+        proof {
+            let tracked mut rest = PointsToRaw::empty();
+            tracked_swap(&mut rest, self.rest.borrow_mut());
+
+            assert(size_of::<V>() as int <=
+                (self.capacity - self.len) * size_of::<V>())
+            by {
+                assert((self.capacity - self.len) >= 1
+                  ==>
+                    size_of::<V>() as int <= (self.capacity - self.len) * size_of::<V>())
+                by(nonlinear_arith);
+            }
+
+            let tracked (points_to_raw, mut rest) = rest.split(size_of::<V>() as int);
+            assume(points_to_raw@.pptr % align_of::<V>() as int == 0);
+            points_to = points_to_raw.into_typed::<V>();
+
+            tracked_swap(&mut rest, self.rest.borrow_mut());
+        }
+
+        let i = self.len;
+        let ptr_usize = self.ptr.to_usize();
+
+        assume(
+            (i as int * size_of::<V>()) as usize as int
+            == (i as int * size_of::<V>()));
+        assume(
+            (ptr_usize as int + i as int * size_of::<V>()) as usize as int
+            == (ptr_usize as int + i as int * size_of::<V>()));
+
+        let elem_ptr_usize = ptr_usize + i * get_size_of::<V>();
+        let elem_ptr = PPtr::<V>::from_usize(elem_ptr_usize);
+
+        elem_ptr.put(Tracked(&mut points_to), v);
+
+        proof {
+            self.elems.borrow_mut().tracked_insert(self.len as nat, points_to);
+        }
+
+        self.len = self.len + 1;
+
+        proof {
+            assert_seqs_equal!(self@, old(self)@.push(v));
+        }
+    }
+}
+
+fn main() { }
+
+}
diff --git a/source/rust_verify_test/tests/cell_lib.rs b/source/rust_verify_test/tests/cell_lib.rs
index 432794ac4e..9db34027b0 100644
--- a/source/rust_verify_test/tests/cell_lib.rs
+++ b/source/rust_verify_test/tests/cell_lib.rs
@@ -54,7 +54,7 @@ test_verify_one_file! {
 }
 
 const PTR_TEST: &str = code_str! {
-    let (ptr, Tracked(mut token)) = PPtr::<u32>::empty();
+    let (ptr, Tracked(mut token), Tracked(dealloc)) = PPtr::<u32>::empty();
     assert(equal(token.view().pptr, ptr.id()));
     assert(equal(token.view().value, Option::None));
 
@@ -75,7 +75,7 @@ const PTR_TEST: &str = code_str! {
     assert(equal(token.view().value, Option::None));
     assert(equal(x, 7));
 
-    ptr.dispose(Tracked(token));
+    ptr.dispose(Tracked(token), Tracked(dealloc));
 };
 
 test_verify_one_file! {
@@ -172,8 +172,8 @@ test_verify_one_file! {
 test_verify_one_file! {
     #[test] ptr_mismatch_put IMPORTS.to_string() + verus_code_str! {
         pub fn f() {
-            let (ptr1, Tracked(mut token1)) = PPtr::<u32>::empty();
-            let (ptr2, Tracked(mut token2)) = PPtr::<u32>::empty();
+            let (ptr1, Tracked(mut token1), Tracked(dealloc)) = PPtr::<u32>::empty();
+            let (ptr2, Tracked(mut token2), Tracked(dealloc)) = PPtr::<u32>::empty();
             ptr1.put(Tracked(&mut token2), 5); // FAILS
         }
     } => Err(err) => assert_one_fails(err)
@@ -182,8 +182,8 @@ test_verify_one_file! {
 test_verify_one_file! {
     #[test] ptr_mismatch_take IMPORTS.to_string() + verus_code_str! {
         pub fn f() {
-            let (ptr1, Tracked(mut token1)) = PPtr::<u32>::empty();
-            let (ptr2, Tracked(mut token2)) = PPtr::<u32>::empty();
+            let (ptr1, Tracked(mut token1), Tracked(dealloc1)) = PPtr::<u32>::empty();
+            let (ptr2, Tracked(mut token2), Tracked(dealloc2)) = PPtr::<u32>::empty();
             ptr1.put(Tracked(&mut token1), 5);
             ptr2.put(Tracked(&mut token2), 5);
             let x = ptr1.take(Tracked(&mut token2)); // FAILS
@@ -194,8 +194,8 @@ test_verify_one_file! {
 test_verify_one_file! {
     #[test] ptr_mismatch_replace IMPORTS.to_string() + verus_code_str! {
         pub fn f() {
-            let (ptr1, Tracked(mut token1)) = PPtr::<u32>::empty();
-            let (ptr2, Tracked(mut token2)) = PPtr::<u32>::empty();
+            let (ptr1, Tracked(mut token1), Tracked(dealloc)) = PPtr::<u32>::empty();
+            let (ptr2, Tracked(mut token2), Tracked(dealloc)) = PPtr::<u32>::empty();
             ptr1.put(Tracked(&mut token1), 5);
             ptr2.put(Tracked(&mut token2), 5);
             let x = ptr1.replace(Tracked(&mut token2), 7); // FAILS
@@ -206,8 +206,8 @@ test_verify_one_file! {
 test_verify_one_file! {
     #[test] ptr_mismatch_borrow IMPORTS.to_string() + verus_code_str! {
         pub fn f() {
-            let (ptr1, Tracked(mut token1)) = PPtr::<u32>::empty();
-            let (ptr2, Tracked(mut token2)) = PPtr::<u32>::empty();
+            let (ptr1, Tracked(mut token1), Tracked(dealloc)) = PPtr::<u32>::empty();
+            let (ptr2, Tracked(mut token2), Tracked(dealloc)) = PPtr::<u32>::empty();
             ptr1.put(Tracked(&mut token1), 5);
             ptr2.put(Tracked(&mut token2), 5);
             let x = ptr1.borrow(Tracked(&token2)); // FAILS
@@ -218,9 +218,19 @@ test_verify_one_file! {
 test_verify_one_file! {
     #[test] ptr_mismatch_dispose IMPORTS.to_string() + verus_code_str! {
         pub fn f() {
-            let (ptr1, Tracked(mut token1)) = PPtr::<u32>::empty();
-            let (ptr2, Tracked(mut token2)) = PPtr::<u32>::empty();
-            ptr1.dispose(Tracked(token2)); // FAILS
+            let (ptr1, Tracked(mut token1), Tracked(dealloc1)) = PPtr::<u32>::empty();
+            let (ptr2, Tracked(mut token2), Tracked(dealloc2)) = PPtr::<u32>::empty();
+            ptr1.dispose(Tracked(token2), Tracked(dealloc1)); // FAILS
+        }
+    } => Err(err) => assert_one_fails(err)
+}
+
+test_verify_one_file! {
+    #[test] ptr_mismatch_dispose2 IMPORTS.to_string() + verus_code_str! {
+        pub fn f() {
+            let (ptr1, Tracked(mut token1), Tracked(dealloc1)) = PPtr::<u32>::empty();
+            let (ptr2, Tracked(mut token2), Tracked(dealloc2)) = PPtr::<u32>::empty();
+            ptr1.dispose(Tracked(token1), Tracked(dealloc2)); // FAILS
         }
     } => Err(err) => assert_one_fails(err)
 }
@@ -228,7 +238,7 @@ test_verify_one_file! {
 test_verify_one_file! {
     #[test] ptr_some_put IMPORTS.to_string() + verus_code_str! {
         pub fn f() {
-            let (ptr1, Tracked(mut token1)) = PPtr::<u32>::empty();
+            let (ptr1, Tracked(mut token1), Tracked(dealloc)) = PPtr::<u32>::empty();
             ptr1.put(Tracked(&mut token1), 7);
             ptr1.put(Tracked(&mut token1), 5); // FAILS
         }
@@ -238,7 +248,7 @@ test_verify_one_file! {
 test_verify_one_file! {
     #[test] ptr_none_take IMPORTS.to_string() + verus_code_str! {
         pub fn f() {
-            let (ptr1, Tracked(mut token1)) = PPtr::<u32>::empty();
+            let (ptr1, Tracked(mut token1), Tracked(dealloc)) = PPtr::<u32>::empty();
             let x = ptr1.take(Tracked(&mut token1)); // FAILS
         }
     } => Err(err) => assert_one_fails(err)
@@ -247,7 +257,7 @@ test_verify_one_file! {
 test_verify_one_file! {
     #[test] ptr_none_replace IMPORTS.to_string() + verus_code_str! {
         pub fn f() {
-            let (ptr1, Tracked(mut token1)) = PPtr::<u32>::empty();
+            let (ptr1, Tracked(mut token1), Tracked(dealloc)) = PPtr::<u32>::empty();
             let x = ptr1.replace(Tracked(&mut token1), 7); // FAILS
         }
     } => Err(err) => assert_one_fails(err)
@@ -256,7 +266,7 @@ test_verify_one_file! {
 test_verify_one_file! {
     #[test] ptr_none_borrow IMPORTS.to_string() + verus_code_str! {
         pub fn f() {
-            let (ptr1, Tracked(mut token1)) = PPtr::<u32>::empty();
+            let (ptr1, Tracked(mut token1), Tracked(dealloc)) = PPtr::<u32>::empty();
             let x = ptr1.borrow(Tracked(&token1)); // FAILS
         }
     } => Err(err) => assert_one_fails(err)
@@ -265,9 +275,9 @@ test_verify_one_file! {
 test_verify_one_file! {
     #[test] ptr_some_dispose IMPORTS.to_string() + verus_code_str! {
         pub fn f() {
-            let (ptr1, Tracked(mut token1)) = PPtr::<u32>::empty();
+            let (ptr1, Tracked(mut token1), Tracked(dealloc)) = PPtr::<u32>::empty();
             ptr1.put(Tracked(&mut token1), 5);
-            ptr1.dispose(Tracked(token1)); // FAILS
+            ptr1.dispose(Tracked(token1), Tracked(dealloc)); // FAILS
         }
     } => Err(err) => assert_one_fails(err)
 }
diff --git a/source/rust_verify_test/tests/size_of.rs b/source/rust_verify_test/tests/size_of.rs
new file mode 100644
index 0000000000..ee367abfaf
--- /dev/null
+++ b/source/rust_verify_test/tests/size_of.rs
@@ -0,0 +1,85 @@
+#![feature(rustc_private)]
+#[macro_use]
+mod common;
+use common::*;
+
+// See https://doc.rust-lang.org/std/mem/fn.size_of.html
+// for stable guarantees about the size of Rust types
+
+test_verify_one_file! {
+    #[test] sizeof_test verus_code! {
+        use vstd::layout::*;
+        use std::sync::Arc;
+        use std::rc::Rc;
+
+        // this size of a pointer/reference should be the same as usize ONLY
+        // for sized types V
+
+        fn test_unsized_wrong<V: ?Sized>() {
+            assert(size_of::<&V>() == size_of::<usize>()); // FAILS
+        }
+
+        fn test_unsized_wrong2() {
+            assert(size_of::<&[u8]>() == size_of::<usize>()); // FAILS
+        }
+
+        // (&mut not supported right now)
+        //fn test_unsized_wrong3<V: ?Sized>() {
+        //    assert(size_of::<&mut V>() == size_of::<usize>()); // FAILS
+        //}
+
+        //fn test_unsized_wrong4() {
+        //    assert(size_of::<&mut [u8]>() == size_of::<usize>()); // FAILS
+        //}
+
+        fn test_unsized_wrong5<V: ?Sized>() {
+            assert(size_of::<Box<V>>() == size_of::<usize>()); // FAILS
+        }
+
+        fn test_unsized_wrong6() {
+            assert(size_of::<Box<[u8]>>() == size_of::<usize>()); // FAILS
+        }
+
+        // I don't think Rust guarantees this, so this should fail.
+
+        fn test_tuple_wrong<A, B>() {
+            assert(size_of::<(A, B)>() == size_of::<A>() + size_of::<B>()); // FAILS
+        }
+
+        // &A and A need to be distinguished
+
+        fn test_ref_distinguished<A, B>() {
+            assert(size_of::<A>() == size_of::<&A>()); // FAILS
+        }
+
+        //fn test_mut_ref_distinguished<A, B>() {
+        //    assert(size_of::<A>() == size_of::<&mut A>()); // FAILS
+        //}
+
+        fn test_box_distinguished<A, B>() {
+            assert(size_of::<A>() == size_of::<Box<A>>()); // FAILS
+        }
+
+        fn test_rc_distinguished<A, B>() {
+            assert(size_of::<A>() == size_of::<Rc<A>>()); // FAILS
+        }
+
+        fn test_arc_distinguished<A, B>() {
+            assert(size_of::<A>() == size_of::<Arc<A>>()); // FAILS
+        }
+
+        // See the explanation in pervasive/layout.rs for why we don't make this assumption.
+
+        fn test_not_assumed_bounded<V>() {
+            assert(size_of::<V>() as usize as int == size_of::<V>()); // FAILS
+        }
+
+        fn test_not_assumed_bounded_align<V>() {
+            assert(align_of::<V>() as usize as int == align_of::<V>()); // FAILS
+        }
+
+        fn test_not_assumed_nonzero<V>() {
+            assert(size_of::<V>() != 0); // FAILS
+        }
+    } => Err(err) => assert_fails(err, 12)
+}
diff --git a/source/vir/src/triggers.rs b/source/vir/src/triggers.rs
index 1c8be1df5e..05649bd5ff 100644
--- a/source/vir/src/triggers.rs
+++ b/source/vir/src/triggers.rs
@@ -46,6 +46,7 @@ fn check_trigger_expr(
             | ExpX::CallLambda(..)
             | ExpX::UnaryOpr(UnaryOpr::Field { .. }, _)
             | ExpX::UnaryOpr(UnaryOpr::IsVariant { .. }, _)
+            | ExpX::UnaryOpr(UnaryOpr::Height, _)
             | ExpX::Unary(UnaryOp::Trigger(_), _) => {}
             // allow triggers for bitvector operators
             ExpX::Binary(BinaryOp::Bitwise(_, _), _, _) | ExpX::Unary(UnaryOp::BitNot, _) => {}