Function tracked_borrow_mut_points_to

Source

pub proof fn tracked_borrow_mut_points_to<K, R, T: Repr<R>>(tracked 
    m: &mut Map<K, PointsTo<R, T>>,
    key: K,
) -> tracked v : &mut PointsTo<R, T>

Expand description

requires

old(m).dom().contains(key),

ensures

*v === old(m).index(key),

v.pptr() === old(m).index(key).pptr(),

v.addr() === old(m).index(key).addr(),

v.is_init() == old(m).index(key).is_init(),

v.wf(&v.inner_perms) == old(m).index(key).wf(&old(m).index(key).inner_perms),

v.inner_perms === old(m).index(key).inner_perms,

final(m).dom() === old(m).dom(),

forall |k: K| k != key ==> (#[trigger] final(m).index(k) === old(m).index(k)),

final(m).index(key) === *final(v),

final(m).index(key).pptr() === final(v).pptr(),

final(m).index(key).is_init() == final(v).is_init(),

final(m).index(key).wf(&final(v).inner_perms) == final(v).wf(&final(v).inner_perms),

Same as tracked_borrow_mut for PointsTo<R, T> values, with the additional open-spec equalities that Verus cannot derive through simple_pptr::PointsTo’s opaque fields.

tracked_borrow_mut_points_to

Function tracked_borrow_mut_points_to Copy item path

Function tracked_borrow_mut_points_to