prove: util::range_alloc - #699
Conversation
|
I think vstd already supports |
|
|
You may also create a PR for Verus. |
|
I will try to investigate |
This comment was marked as off-topic.
This comment was marked as off-topic.
| &&& old_map[*key] == old_value | ||
| &&& new_map == old_map.insert(*key, new_value) | ||
| }, | ||
| ; |
There was a problem hiding this comment.
Why do we need this function and axiom? Does this just mean insert?
There was a problem hiding this comment.
This axiom provides a concrete interpretation of borrowed_key_mutated when the borrowed lookup key has the same type as the key stored in the map.
The generic BTreeMap::get_mut specification must support borrowed-key lookups where the types differ, such as BTreeMap<String, V>::get_mut(&str). In that case, the borrowed key cannot generally be converted back into the exact stored key, so the specification uses the abstract relation borrowed_key_mutated.
When the borrowed and stored key types are both Key, the relation can be characterized precisely:
- The key existed in
old_map. - Its value was
old_value. new_mapisold_mapwith that key mapped tonew_value.
Therefore, this is not specifying a call to executable BTreeMap::insert. The spec-level Map::insert is a functional update used to describe the final mathematical state of the map. The axiom also records the successful lookup and the previous value.
Declaring it as a broadcast axiom allows Verus to apply this interpretation automatically when reasoning about get_mut with identical borrowed and stored key types.
There was a problem hiding this comment.
This definition is very weird. Because the whole system only works when Q is identical to Key. A more general way may be to add a borrow_spec to the Borrow trait. Then we can have some definition like exists |k: Key|, old_map.contains(key) && key.borrow_spec() == q && new_map == old_map.insert(k, new_value). Next we can add a broadcast lemma that handles the identical case, which removes the exists quantifier. However, this will require a fundamental change to Borrow's spec, which is undefined now. You can find it in std_specs/core.rs. You'd better open a question about how to support the general Borrow trait in Verus Zulip first.
| Some(value) => borrowed_key_mutated(old(map)@, final(map)@, key, *value, *final(value)), | ||
| None => !contains_borrowed_key(old(map)@, key) && final(map)@ == old(map)@, | ||
| }, | ||
| ; |
There was a problem hiding this comment.
It is incorrect that this function does not have any preconditions. According to the std documentation, the ordering of Q must match the ordering of Key. This precondition is not expressed here.
There was a problem hiding this comment.
And I find this one is also related to borrow_spec. Maybe we can merge the version without btree_map::CursorMut and BTreeMap::get_mut first. The borrow_spec needs to be discussed with Verus developers
There was a problem hiding this comment.
Maybe we can merge the version without
btree_map::CursorMutandBTreeMap::get_mutfirst.
Yes, I agree.
b2ff64e to
60daf60
Compare
|
Verus's external specification of Borrow |
Marsman1996
added
AI-assist
| { | ||
| &&& borrowed_key_removed(old_map, remainder, key) | ||
| &&& borrowed_key_removed(new_map, remainder, key) | ||
| } |
There was a problem hiding this comment.
Why do we need this exists clause?
There was a problem hiding this comment.
The existential clause is the frame condition for get_mut. The preceding predicates only constrain the value associated with the borrowed key; without this clause, the specification would also allow arbitrary changes to every other entry. Requiring both maps to produce the same remainder after removing the borrowed key ensures that they differ only at that entry. We use borrowed_key_removed because, for a general Key: Borrow<Q>, Verus currently has no borrow_spec that lets us directly identify the corresponding stored Key.
For the Q = Key case used by range_alloc, the existential clause reduces to:
old_map.remove(*key) == new_map.remove(*key)Together with the two value-mapping predicates, this states that only the value corresponding to key may change; all other entries remain unchanged. This matches BTreeMap::get_mut, which returns a mutable reference to the value corresponding to the borrowed key.
The borrowed_key_ordering_matches precondition separately captures the documented requirement that the ordering of Q must match the ordering of Key.
For an arbitrary heterogeneous Key: Borrow<Q>, this remains an abstract specification because vstd does not yet formalize the semantics and ordering laws of a general Borrow implementation. However, it is precise for the Q = Key case used here.
60daf60 to
24246c2
Compare
2 participants
The 3#[verifier::external_body]are caused by theBTreeMapThis PR is parsed into 3 (including this one):
#[verifier::external_body]