First, we prove the adequacy theorem for STLC. We have no state and therefore no (fancy) update modalities, so we do not need any lemmas handling them.
We prove the weak adequacy theorem for a language
We prove the weak adequacy theorem with later credits in the logic, but without later credits in the weakest precondition.
Here, we assume ownership of all later credits in the proof of the adequacy theorem, i.e. lc_supply n * £ n. In practice, this means that the user cannot spend any of the later credits, hence this setting is practically equivalent to having no later credits in the logic.
We also prove the weak adequacy theorem when we have later credits in the weakest precondition.
We do the proof of the weak adequacy theorem with later credits in the logic and in the weakest precondition, with a proof structure using only "current" Iris lemmas, i.e. not the ones with the half fancy update modality.
We prove the strong adequacy theorem with no later credits in the logic using the new lemmas (half fancy update modality).
We also show the old proof from before later credits were added to the logic.
We prove the strong adequacy theorem with later credits in the logic, but without later credits in the weakest precondition.
We also prove the strong adequacy theorem when we have later credits in the weakest precondition.
