Sorry to bring this up again, I just think it's important to get this as right as we can, right now. ;)
This moves the global functor and dynamic composeable ownership to base_logic. The reasoning behind this is that if someone builds another program logic in our base logic, they will likely want to re-use this, so it makes more sense to have it in base_logic than in program_logic.
The rule for stuff to be in program_logic is: It depends on the Iris' notion of a language, or on world satisfaction (i.e., on our specific way to do invariants). Thus, saved_prop also moves to base_logic and becomes reusable by other program logics.
(If we want, we can talk about changing this to just "anything that depends on our notion of a language". Is it conceivable that our world satisfaction is reusable?)
When we talked about this previously, Robbert raised concerns about the name iProp. However, considering that we also have iTactics and use I for the uPred_scope, I feel like the letter "i" has already leaked way beyond program_logic, so this PR doesn't actually change anything. If you want, interpret iProp as "internal propositions", that even makes sense. ;)