Skip to main content

tracked_borrow_mut

vstd_extra::map_extra

Function tracked_borrow_mut 

Source 
pub proof fn tracked_borrow_mut<K, V>(tracked m: &mut Map<K, V>, key: K) -> tracked v : &mut V
Expand description
requires
old(m).dom().contains(key),
ensures
*v == old(m).index(key),
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),

Borrows an entry from a tracked Map mutably.

Returns &mut v where v = old(m)[key]. While the returned borrow is live, m is exclusively held; at its end, m[key] equals whatever v ended up being, and all other entries are unchanged.

This is the mutable counterpart to Map::tracked_borrow and mirrors PointsTo::borrow_mut_inner_perms in structure.