cap_machine.exercises.cerise_tutorial

This file is a tutorial to learn how to use the Cerise Program Logic within Coq. We will specify a simple program and explain how to use the tactics of the Cerise Proofmode to prove the specification. Prerequisites: We assume the user already knows how to use Iris and the Iris Proofmode, for instance with Heaplang. Learning material for Iris is available at this URL: https://iris-project.org/

The imports correspond to the following:

• the Iris tactics and the Iris proofmode
• the WP rules of the Cerise program logic
• the automated tactics of the Cerise proofmode
• some additional tactics for the Cerise proofmode

We recommand to check the documentation of the proofmode of Cerise: https://github.com/logsem/cerise/blob/main/proofmode.md

Iris requires the ressources in the context. The resources of our machine are the registers and the memory. Moreover, we need the machine parameters in the context, which abstract the encoding and the decoding function (for instance, to encode the instructions).

The program is a list of instructions. As the machine has a Von Neumann architecture, the instructions are encoded data. The function `encodeInstrsW` transforms a list of instructions into integers. The encoding does not matter, as we always manipulate the encoded instructions with the decoding function. The program we will study in this file moves a pointer in a buffer and stores a value at this new location. More precisely, we assumes that the register `r1` of the machine contains a capability pointing to a memory buffer of size >= 1. The program derives a capability to the next address, and stores the value of the register `r2` at this address.

We use the program logic to specify the program. In the program logic, there is 2 types of ressources:

• the register /reg/ maps to the word /w/, reg ↦ᵣ w
• the address /a/ maps to the word /w/, a ↦ₐ w.

The notation [a1, a2] ↦ₐ [lw] maps the list of String.words /lw/ to the contiguous fragment of memory between the adresses /a1/ and /a2/. To write the specification, we need to have the separation logic assertion that describe all the resources required throughout the execution. In this case, we need the ownership of:

• the fragment of the memory with the instructions of the program, stored between the adresses `a_prog` and `a_prog + len(prog)`
• the memory buffer on which the program stores the new value, between the addresses `b_mem` and `b_mem + 2`
• the PC contains a capability pointing to the first addresse of the program `a_prog`, with all the required permissions (i.e. validity range and executable)
• the registers `r1` and `r2`, where `r1` contains the capability to the buffer and `r2` contains the new data (in our case, 42)

The usual way to specify a program in Cerise in Coq is to use the weakest-precondition (WP) with a Continuation Passing Style, instead of the Hoare Triples. The CPS style is defined as follows: {P} e {Q} ≡ ∀ ϕ, (P ∗ ▷(Q -∗ WP e { ϕ })) -∗ WP e { ϕ } It is important to notice that, for a such low-level programming language, there is no notion of expression. The semantic only describes how the state of the machine changes at each execution step, as soon as the machine is in a Running state. However, the WP property requires an expression. In this way, an expression in the Cerise program logic encodes only the execution state of the machine (Running, Halted or Failed) (1). Thus, the WP rules only describes how the resources of the machine evolve at each execution step. (1) For technical purpose, an expression in actually either a (non-atomic) Sequence of instructions, or an (atomic) Instruction. The following lemma `prog_spec_instr` is a specification of the program previously defined. The SL assertion for the fragment of code is `codefrag a_prog prog_instr`. The PCC (PC Capability) has the permission `pc_p`, which has, at least, the execution permission: `ExecPCPerm p_pc`. The validity range of the PCC, between the addresses `pc_b` and `pc_e`, is larger than the actual range of the code fragment. Indeed, for modular purposes, the program we are specifying may be a part of a larger program. Thus, we need to ensure the fragment of the code is included in the PCC range, i.e. `SubBounds b_pc e_pc a_prog e_prog`. Because we work with addresses, which are actually finite integers, we need to assume the addresses are always valid when we do addresses arithmetic operations (for instance, there is no overflow of the memory). In particular, the memory buffer is a contiguous region of memory where all the addresses are in the bounds of the memory. For simplicity, we assume the buffer is filled with 0. When the whole program is a list of instructions, it is required to manually get some helping facts before reasoning on the instructions, using the tactic `codefrag_facts "Hprog"`. This tactic has to be used when the `codefrag` assertion is used. It allows to get some additionnal facts about the memory addresses containing the code. It is a boilerplate. To prove the specification, the idea is to manipulate the resources, such that we have all the required assertion that fit with the corresponding WP rule. Once all the resource are ready, the tactic `iInstr "Hprog"` steps through one instruction, automatically finds the appropriate rule, and tries to discharge as much goal as possible (e.g. side-condition about the PC). It only remains some side-condition to prove manually, such as address arithmetic. We can use the tactic `solve_addr` to solve automatically the address arithmetic goals. It sometimes requires to transform the goal or hypotheses a bit to work. We advice to read carefully the following specification and to try to understand each statement in the lemma. Then, we urge to execute the proof step by step, and to understand each time what happens to the proof state and why we are doing it.

The tactic `iGo "Hprog"` steps through multiple instructions, until a side-condition needs to be prove manually.

Exercise 1 --- More automation with iGo

Prove the specification of the previous example using the automated tactic `iGo`. In order to leverage the strengh of the tactic, the memory resources should be ready before the execution of the tactic, in particular, the memory buffer should be split at the beginning of the proof: it will allows the tactic `iGo` to step through multiple instructions at once. Tips: take inspiration on the proof of the previous exercise, but we recommend to try to manipulate the SL resources and the address arithmetic by yourself. Indeed, address arithmetic is a very common side-condition, and the lemmas often require you to manipulate the PL resources in order to make them fit with the hypothesis.

The tactics `iInstr` and `iGo` automatically lookup the PC, find the corresponding instruction in the `codefrag` instruction, find the right WP rule to apply accordingly with the instruction, instantiate the lemma and try to prove as much precondition as possible. However, in order to get a better understanding of the way to use the WP rules in Cerise, we propose to prove the previous lemma using the fully detailed tactics. It is also useful if the assertion that embeds the code is not the `codefrag` predicate, but for instance, the big conjonction separation `∗ list` --- even though it is usually possible to rewrite the one in term of the other.

Exercise 2 --- Manual detailled proofs

For this exercise, we propose to re-do the proof of the previous specification, using the manual WP rules. We explain the different steps for the first instruction `Lea`. Complete the proof.

The next step to learn how to use the Cerise Proofmode is to leverage the modularity of program logic to define macros and use their specification inside bigger programs. The next part of the tutorial "cerise_modularity.v" will learn you how to define, specify and use user-defined macros, and present you the main macros already defined in Cerise.