Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657#![allow(unused_imports)]
use super::pervasive::*;use super::prelude::*;use super::proph::*;
verus! {
pub ghost struct MutRef<'a, T: ?Sized> { pub ptr: *mut T, pub current: &'a T, pub future: ProphecyGhost<&'a T>,}
impl<'a, T: ?Sized> MutRef<'a, T> { pub uninterp spec fn pack(self) -> &'a mut T;
pub uninterp spec fn unpack(r: &'a mut T) -> Self;}
pub broadcast axiom fn axiom_unpack_mut_ref_current<T>(a: &mut T) ensures mut_ref_current(a) == (#[trigger] MutRef::unpack(a)).current,;
pub broadcast axiom fn axiom_unpack_mut_ref_future<T>(a: &mut T) ensures mut_ref_future(a) == (#[trigger] MutRef::unpack(a)).future.value(),;
pub broadcast axiom fn axiom_unpack_pack<T: ?Sized>(data: MutRef<T>) ensures MutRef::unpack(#[trigger] data.pack()) == data,;
pub uninterp spec fn pack2<'a, T: ?Sized>(data: MutRef<'a, T>) -> &'a mut T;
pub broadcast axiom fn axiom_pack2_unpack<T: ?Sized>(a: &mut T) ensures pack2(#[trigger] MutRef::unpack(a)) == a,;
pub axiom fn borrow_prophecy_var<'a, 'b, T: ?Sized>(tracked m: &'a &'b mut T) -> (tracked t: &'a ProphecyGhost<&'b T>) ensures t.value() == &*final(*m),;
pub broadcast group group_mut_ref_axioms { axiom_unpack_mut_ref_current, axiom_unpack_mut_ref_future, axiom_unpack_pack, axiom_pack2_unpack,}
} // verus!