5.1. Introduction🔗

Now that we have seen basic separation logic in Iris and introduced a suitable language, HeapLang, we are finally ready to start reasoning about programs. HeapLang ships with a program logic defined using Iris. We can access the logic through the proof-mode package, which also defines tactics to alleviate working with the logic.

The program logic for HeapLang relies on a basic notion of a resource: the resource of heaps. Recall that GF specifies the available resources. To make the resource of heaps available, we require an instance of HeapLangGS hlc GF throughout this section. This corresponds directly to the Rocq tutorial's Context {!heapGS Σ} (with a backtick before the brace).