fix SIFA logic

[RalfJung]

At least I think the old logic was wrong? Cc @JoJoDeveloping

The old logic was based on this comment:

/// For all non-accessed locations in the RangeMap (those that haven't had an
/// implicit read), their SIFA must be weaker than or as weak as the SIFA of
/// `default_perm`.

This should have said "must be at least as strong as", right? The invariant is that "the SIFA at each child must be stronger than that at the parent", so having stronger things in the new node should always be fine.

We should definitely have a test for this, if possible (but it may be that this doesn't actually lead to any bugs due to the implicit read fixing things up).

[rustbot]

Thank you for contributing to Miri!
Please remember to not force-push to the PR branch except when you need to rebase due to a conflict or when the reviewer asks you for it.

[RalfJung]

I think this is the actual assertion we needed before I added the max earlier today:

// Accessed nodes have the SIFA fixed up as part of the access. For everything else,
// let's ensure default_strongest_idempotent has the minimum SIFA so the fixup
// below does the right thing.
if !perm.accessed {
    assert!(default_strongest_idempotent <= perm.idempotent_foreign_access);
}

This assertion also passes. The thing we checked instead (default_strongest_idempotent >= perm.idempotent_foreign_access) seems just entirely pointless, but it also passed since for non-accessed nodes we in fact always have default_strongest_idempotent == perm.idempotent_foreign_access (because if a non-accessed node exists, then outside_perm is the same as nonfreeze_perm).

[JoJoDeveloping]

can we add an assert here that perm.idempotent_foreign_access == perm.permission.strongest_idempotent_foreign_access(protected)? I do not fully recall what sets perm.idempotent_foreign_access initially and since it's "far away" from this function it might be easy to miss that this is used here.

[RalfJung]

The constructor sets it and it's a private field so nobody outside this files can mess with it, but sure.

[JoJoDeveloping]

Good catch!