Function positioned_at_upper_bound 

pub open spec fn positioned_at_upper_bound<Key, Value, Q: ?Sized>(
    model: CursorMutModel<Key, Value>,
    bound: Bound<&Q>,
) -> bool

{
    &&& forall |i: int| {
        0 <= i < model.position ==> before_upper_bound(model.keys[i], bound)
    }
    &&& forall |i: int| {
        model.position <= i < model.keys.len()
            ==> !before_upper_bound(model.keys[i], bound)
    }

}

Whether a cursor is at the gap selected by upper_bound_mut.