3.1. Pre- and Postconditions🔗

First, we need to understand what our program is doing. Once this is clear, we want to express this in first-order predicate logic.

Let's take a look at some examples:

We expect that after executing this program, registers x_1 and x_2 will contain the values that were loaded into them, and register x_3 will contain the result of adding x_1 and x_2. That means the specification of this code snippet looks like this: x_1 = 1 \wedge x_2 = 43 \wedge x_3 = x_1 + x_2

The next example involves a loop:

In this code, we have no concrete values, but some variables. This makes the specification more general, and we do not restrict the specification to specific values. So let's see what is happening here:

First, an address addr is loaded into a register regWithAddr. Then, the loop is entered. It starts with a conditional jump, which happens when the content of a register counter equals zero. If that is the case, we jump to the label finish. When the register holds a value greater than zero, the actual loop body is entered. The content of a register regWithValue is stored in the memory at the address that the register regWithAddr holds. Once this is done, the address inside the register regWithAddr is incremented by one, the value the register counter holds is decremented by one, and we jump back to the label loop.

Let \text{memory}(n) denote the memory address n \in \mathbb{U}_{64}. Then, the specification of this program could be formulated as follows:

\begin{aligned} \text{Pre} \; \coloneqq \; & i < \text{length} \;\wedge\; \text{addr} + \text{length} - 1 < 2^{64} \\[0.5em] \forall i \in \mathbb{U}_{64},\; & \text{Pre} \;\rightarrow\; \text{memory}(\text{addr} + i) = x_{\text{regWithValue}} \end{aligned}

So as you can see, we need several things to successfully write down a correct specification:

1. First-order logic with arithmetic expressions

2. Access to the values (registers, memory, etc.) of a certain machine state

Luckily, 1. is already provided by Lean itself, so we just need to somehow access a machine state. MRiscX offers a simple way to do this.

Inside the ⦃⦄ braces, we can write down first-order logic formulas just as we do in usual terms of type Prop. Additionally, there are the following custom terms which can be used:

• ⸨terminated⸩

  This term is the MState.terminated flag. It indicates whether the program has terminated and whether the current machine state is legal. If this flag is true, the machine state is no longer legal, and no further instructions can be executed. Consequently, ⦃¬⸨terminated⸩⦄ serves as a precondition that is almost always required to ensure that instructions can be executed and, ultimately, to establish the functional correctness of a program.

• ⸨pc⸩

  With this term, we can define the value of the MState.pc. Using this, we can ensure that the MState.pc holds a certain value before or after executing a program. Note that l also ensures that the MState.pc points to a certain line before executing the program, so this term is often only useful in the postcondition.

• x[n], where n is either a number of type UInt64 or an identifier (Lean.Parser.ident)

  Using this term, we can specify a value n for a register x_n in MState.registers. As already mentioned, this n can either be a number of type UInt64 or an identifier. This means that the terms

  variable (n v : UInt64) fun st => st.getRegisterAt n = v : MState → Prop#check ⦃x[n] = v⦄ fun st => st.getRegisterAt 1 = 42 : MState → Prop#check ⦃x[1] = 42⦄ fun st => st.getRegisterAt 1 = 17425 : MState → Prop#check ⦃x[1] = 0x4411⦄

  are all legal. Also note that Lean inherently supports hexadecimal numbers, so ⦃x[1] = 0x4411⦄ is legal and can (and should) be used to describe that a certain register holds a memory address.

• mem[t], where t is a Lean.Term. This includes every custom term presented here.

  This term can be used to define the value at a specific location in the MState.memory. Since it is possible to use the regular terms of Lean as well as the newly introduced custom terms, we can load an address into a register, manipulate it, and then use this register inside the square brackets.

  fun st => st.getMemoryAt 140730297737284 = 4123 : MState → Prop#check ⦃mem[0x7ffe5367e044] = 4123⦄ fun st => st.getMemoryAt (st.getRegisterAt 2 + 1) = st.getRegisterAt 4 + st.getRegisterAt 5 : MState → Prop#check ⦃mem[x[2] + 1] = x[4] + x[5]⦄

• labels[i], where i is of type Lean.Ident.

  Using this, we can ensure either that the label i exists on a specific line or that it does not exist at all. Note that the labels inside the code sections are already stored in Code.labels, so they do not need to be specified within the pre- or postconditions.

  This term returns an Option UInt64.

  fun st => st.getLabelAt "first" = some 0 : MState → Prop#check ⦃labels[first] = some 0⦄ fun st => st.getLabelAt "_L_store" = none : MState → Prop#check ⦃labels[_L_store] = none⦄

To wrap things up, here is an example of a Hoare triple with some of the terms presented:

3.2. Program Counter, Blacklist, and Whitelist🔗

As already shown in the introduction of Hoare logic, we need to specify exactly where the ProgramCounter points to before executing the program. Also, we need to provide a blacklist and a whitelist in order to ensure that the ProgramCounter only visits the lines we intend to prove the formal correctness of. The ProgramCounter is of type UInt64 and the blacklist and whitelist are of type Set UInt64. We can use the usual syntax here.

The value required for the ProgramCounter is the line which the PC points to before executing the first instruction. So basically, this should be the first instruction we want to be executed. After executing one instruction, the ProgramCounter points to the next instruction.

We define the whitelist as a set of lines that contains any lines the PC might point to after the program has terminated.

So if we have a program like this:

the Hoare triple should look like this

As you can see, we want to stop when the PC points to line 1, that is, the line immediately following the instruction we want to inspect. To make explicit something that can be slightly confusing when defining a Hoare triple, we write {n : UInt64 | n > 1} ∪ {0} (which is simply a cumbersome way of writing {n : UInt64 | n ≠ 1}) as the blacklist. This choice is motivated by the fact that the weak function only considers machine states that have executed at least one instruction. Consequently, if we want to ensure that the PC does not visit the line where the first instruction is located after at least one instruction has been executed, we must include this line in the blacklist.