As you can see, to write code, use the keywords mriscx and end.
Between these keywords, you can define labels and RISC-V instructions.
It is not permitted to have instructions without a label as their "parent", but you may
have labels without any instructions (see the finish label in the example).
Additionally, each instruction must be followed by a newline (or a semicolon).
Note: Unfortunately, in the current version of MRiscX, a space in the register name
between the x and the number is required. This is due to the syntax extension as
provided by Lean.
Note: Due to the elaboration, the actual syntax does not require a String
but an identifier (ident). Therefore, there is no need to use quotation
marks to represent a sequence of characters as a string type.
This is also true for all the following conditional jump instuctions
Hoare logic is a formal system for verifying the correctness of structured
imperative programs
Structured Programming := Programming,
that does not use goto..
Its goal is to enable the precise formulation and proof of statements about
program behavior.
To this end, Hoare logic provides a set of logical rules that support rigorous
reasoning about the correctness of computer programs.
At its core, Hoare logic combines two key ideas: expressing program
specifications in a clear and
natural way, and applying a structured proof technique to show that programs
satisfy these
specifications. The term structured refers to the fact that the structure of
the proof mirrors the
structure of the program itself. This logic was first introduced by
Hoare (1969)Charles Antony Richard Hoare (1969). “An axiomatic basis for computer programming”. Communications of the ACM.12 10pp. 576–580..
A central element of Hoare logic is the Hoare triple. A Hoare triple
is a statement about the state of a machine before and after the execution
of a command. By default, such a triple is notated as follows:
\{P\} c \{Q\}
P and Q are logical statements about the state before and after the
execution of the program segment c.
What exactly these statements describe depends on the structure of the
respective machine state.
For example, they may refer to variable assignments, the contents of memory,
register values, or the value of the program counter.
The Hoare triple now states:
If command c begins execution in a state that satisfies statement P,
and if c eventually terminates in a state, then that final state satisfies
statement Q.
The statement P is called the precondition of the
triple, and Q is the
postcondition.
Example:
{x = 0} x := x + 1 {x = 1}
This Hoare triple states:
If a state satisfies x=0 and the code x := x + 1
is executed, then the resulting state satisfies x = 1.
The “original” Hoare logic cannot be applied without restriction to all programs
or architectures. In structured programming, there are no restrictions on the
application of Hoare logic, as the sequence of commands is precisely defined.
It is always clearly defined which command
will be executed next, and there is no possibility of jumping to any arbitrary
command. A sequential chain is formed in which each link must be executed one
after the other. This is not the case in unstructured programming
Unstructured Programming := Programming, that uses goto.
Jump commands such as goto can be used to jump to any point in
the code.
Due to these restrictions on control flow and the limited ability
to reason about intermediate program points—which is required to support complete
correctness—the “classical” Hoare triples are unsuitable for unstructured programs
(Lundberget al, 2020)Didrik Lundberg, Roberto Guanciale, Andreas Lindner, and Mads Dam, 2020. “Hoare-style logic for unstructured programs”. In International Conference on Software Engineering and Formal Methods..
Since MRiscX contains elements of unstructured programming,
an extended form of Hoare logic is used, as presented by Lundberget al (2020)Didrik Lundberg, Roberto Guanciale, Andreas Lindner, and Mads Dam, 2020. “Hoare-style logic for unstructured programs”. In International Conference on Software Engineering and Formal Methods..
In the following, the function MState.runOneStep executes a single instruction,
thereby transforming a machine state s into a successor state s'.
The function MState.runNSteps denotes the n-th iteration of MState.runOneStep.
Furthermore, MState.pc returns the line to which the ProgramCounter points in a
given machine state s.
Within this framework, MState.runOneStep corresponds to the function nxt, and
MState.pc corresponds to the function lbl from the
weaktransition relation introduced in
(Lundberget al, 2020)Didrik Lundberg, Roberto Guanciale, Andreas Lindner, and Mads Dam, 2020. “Hoare-style logic for unstructured programs”. In International Conference on Software Engineering and Formal Methods..
Using these definitions, the weaktransition relation in MRiscX is formalized as
follows:
This weak relation, inspired by Lundberg et al. (2020),
is defined over two MStates, s and s'.
Unlike earlier formulations that take a single set of lines L,
this relation is parameterized by two sets of lines, L_w and L_b.
This design has the advantage that the condition s'.pc∈L_w is already guaranteed
by the relation itself. Since we assume L_w∩L_b=∅, it immediately follows that
s'.pc∉L_b must also hold. Consequently, the explicit postcondition s'.pc∈L_b in
the Judgment ofL_as could be omitted. However, this simplification has not yet been
applied in the current version.
This relation is defined as follows:
State s' is reached from state s after exactly n steps, where n>0, and the program
counter of s' points to a line in L_w. Moreover, there exists no n'∈ℕ with 0<n'<n
such that the state reached after n' steps from s has its program counter in L_w∪L_b.
In other words, s' is the first state along the execution path whose program counter lies
in L_w.
The weak relation is deterministic and partial: a program starting in s may never reach a
state whose program counter lies in L_w. Additionally, the relation guarantees that no
intermediate state between s and s' has a program counter in L_w.
With the help of this relation, unambiguous statements can be made about the flow of the program.
To be able to reason about a given machine state (MState), we need the function
Assertion.
The weaktransition relation has two machine states,
s and s', and two sets of lines, L_W and L_B, as arguments.
This relation now states the following:
If n \in \mathbb{N} and n > 0 steps are taken from state s, state s' is reached.
The PC of s' points to a line that is an element of L_W.
Furthermore, there is no n' \in \mathbb{N} with 0 < n' < n
such that after n' steps from state s, a state is reached whose PC also points to a
line that is an element of L_W \cup L_B (Lundberget al, 2020)Didrik Lundberg, Roberto Guanciale, Andreas Lindner, and Mads Dam, 2020. “Hoare-style logic for unstructured programs”. In International Conference on Software Engineering and Formal Methods..
L_W is referred to as the whitelist and L_B as the blacklist.
The weaktransition relation is deterministic and partial,
since a program that starts in s may never reach L_W.
It also guarantees that no intermediate state s'' exists between s and s' with
s''.pc\in L_W \cup L_B.
With the help of this relation, unambiguous statements can be made about the flow of the program.
In order to formulate a Hoare triple, the function hoare_triple_up can be used.
This function is inspired by the
\text{judgment of } \mathcal{L}_\text{AS} in (Lundberget al, 2020)Didrik Lundberg, Roberto Guanciale, Andreas Lindner, and Mads Dam, 2020. “Hoare-style logic for unstructured programs”. In International Conference on Software Engineering and Formal Methods.
Inspired by the judgementofL_{as} in the paper Lundberg et al. (2020).
Suppose, that L_w∩L_b=∅ and L_w≠∅ hold, then the hoare_triple_up means:
For all states s in which both P(s) and I(s) are satisfied and whose
program counter points to l,
there exists a successor state s' for which both the relation
weak(s,L_w∪L_b,s') and Q(s'), I(s') and s'.pc∉L_w
are satisfied.
The notation introduced for a Hoare triple looks like this:
, where P and Q represent the pre- and postconditions; l is the line the PC points to
before executing the first instruction; L_W is the whitelist; and L_B is the blacklist.
In (Hoare, 1969)Charles Antony Richard Hoare (1969). “An axiomatic basis for computer programming”. Communications of the ACM.12 10pp. 576–580., Hoare provides rules
that can be used to navigate through a proof of formal correctness of a program
using Hoare logic.
Those rules were transferred to \mathcal{L}_\text{AS} by Lundberget al (2020)Didrik Lundberg, Roberto Guanciale, Andreas Lindner, and Mads Dam, 2020. “Hoare-style logic for unstructured programs”. In International Conference on Software Engineering and Formal Methods.,
except for the axiom of assignment. In the following, the transferred rules are going to be
presented in two ways. First, the notation from the paper by Lundberget al (2020)Didrik Lundberg, Roberto Guanciale, Andreas Lindner, and Mads Dam, 2020. “Hoare-style logic for unstructured programs”. In International Conference on Software Engineering and Formal Methods. is
shown, followed by the implementation in MRiscX in Lean.
The notation used below should be understood as follows:
Everything above the line represents the prerequisites.
In the case of the rule axiom of assignment, there are no prerequisites,
but all other rules do have prerequisites.
The terms below the line indicate the conclusions that can be derived from the
assumptions.
A very elemental Hoare rule is the axiom of assignment:
\frac{}{\{P [x \leftarrow f]\} \quad x \leftarrow f \quad \{P\}} \quad
\textrm{\scriptsize axiom of assignment}
This rule means that if x is a variable identifier and f is an expression, then
P[x \leftarrow f] is created by replacing all occurrences of x in P with f.
The next two rules come from the rule of consequence, which allows us to derive new statements about
a given Hoare triple. In (Lundberget al, 2020)Didrik Lundberg, Roberto Guanciale, Andreas Lindner, and Mads Dam, 2020. “Hoare-style logic for unstructured programs”. In International Conference on Software Engineering and Formal Methods., this rule was split into two to
avoid unnecessary calculations when implementing proof procedures:
The rule PRE-STR, which allows us to strengthen the precondition of a Hoare triple:
(\models (\mathbf{lbl} = l) \wedge P_2 \implies P_1)
\frac{[P_1]l \rightarrow \langle L_W | L_B \rangle [Q]}
{[P_2]l \rightarrow \langle L_W | L_B \rangle [Q]}
\quad \textrm{\scriptsize PRE-STR}
Enables the merge of two Hoare-triples into one, given that the postcondition
of the first triple is equal to the precondition of the second triple.
This rule lets you apply S_SEQ with any form of L_{B''} but asks for
a proof of L_{B''}=L_B∩L_{B'}
This rule states that if both Hoare triples \{P\} c_1 \{R\} and
\{R\} c_2 \{Q\} hold, they can be combined to derive the Hoare triple
\{P\} c_1; c_2 \{Q\}, where c_1; c_2 means that the programs c_1 and c_2 are
executed in sequence.
Note that the starting point of the second command sequence may consist of multiple lines
contained in L_W.
The precondition L'_W \subseteq L_B ensures that none of the final lines have already
been visited in the first segment (l \rightarrow \langle L_W \mid L_B \rangle).
To avoid any ambiguity regarding visited lines, we additionally assume that
L_W \cap L'_W = \emptyset.
An essential function in computer programs is the use of loops, which execute a chain of commands
repeatedly until a certain condition C no longer applies.
Such a loop can be created in unstructured programs using a jump command such as j or goto.
In order to prove statements about
programs with loops, the rule S-LOOP is required. To apply this rule, a loop condition C,
a loop invariant I and a loop variant V are required.
The special feature of I is that it is a statement that is true both before and after each loop
iteration.
Therefore, I remains valid regardless of the number of loop iterations—even if the loop is not
executed a single time.
By contrast, the loop variant serves a different purpose.
The loop variant is an element or statement V from a well-ordered set
W with < as the order relation.
Due to the well-ordering, the set W has a smallest element, which means that there cannot
be an infinite chain with x_1 > x_2 > \dots. It now needs to
be shown that the value of V decreases strictly monotonically, i.e., it decreases after
each loop iteration.
If this can be shown, the loop must terminate at some point, since the value of V can only
decrease a finite number of times.
For this proof, the variable x is introduced, which is not used in any other way within a
program.
This entire concept is formalized in the rule S-LOOP as follows:
\begin{pmatrix}
\models l \notin L_W \\
\models l \notin L_B
\end{pmatrix}
\frac{
\begin{matrix}
[C \wedge I \wedge V = x]
l \rightarrow \langle \{l\} \cup L_W | L_B \rangle
[\textrm{\textbf{lbl}} = l \wedge I \wedge V < x] \\
[\neg C \wedge I]l \rightarrow \langle L_W | L_B \rangle [Q]
\end{matrix}
}
{[I]l \rightarrow \langle L_W | L_B\rangle [Q]}
\quad \textrm{\scriptsize S-LOOP}
A rule to verify the formal correctness of a loop.
Requires:
A Condition C
An Invariant I
A Variant V
For more information, see the (documentation)[https://docs.mriscx.dev/Fundamentals/#sloop]
The rule S-LOOP describes two states of a loop.
On the one hand, there is the loop itself, which is bound to condition C and contains both the
loop invariant I and the loop variant V. The union of \{l\} and L_W and the
postcondition \mathbf{lbl} = l ensure that at the end of a loop iteration, the PC points back
to the beginning of the loop.
On the other hand, there is the case where \neg C applies. Under these circumstances,
the loop body is exited, and a jump is made to one of the lines stored in L_W.
Since \mathcal{L}_\text{{AS}} works with sets of program lines, rules are needed to
be able to adjust them during a proof.
For this purpose, the following three rules were defined in Lundberget al (2020)Didrik Lundberg, Roberto Guanciale, Andreas Lindner, and Mads Dam, 2020. “Hoare-style logic for unstructured programs”. In International Conference on Software Engineering and Formal Methods.,
which allow the contents of the sets L_W and L_B to be manipulated.
This rule can be used to transfer the set L from L_W to L_B.
However, this requires that the postcondition Q does not cause the PC
to point to a line from L.
For certifying the instruction, the ruleofassignment (P ⟦x[r] ← v; pc++⟧) is used.
The hoare triples state that if you start in a state where the precondition P holds,
and you execute the instruction, the precondition P will still
hold after the execution. The precondition is applied after simulating the
effects of the instruction.
By defining the specification for every available instruction and delivering a proof,
the formal correctness of the interpreter is shown.