First Steps for Later Credits
This merge request is the first step to integrate later credits into Iris. It adds all the required infrastructure (i.e., the later credits, the update modalities, and the adequacy proof) without touching the rules of the program logic just yet.