Documentation MRiscX

4. Process of Proving Formal Correctness🔗

To enable a better user experience while proving the formal correctness of an implementation in RISC-V assembly, some custom tactics were implemented. These tactics enable multiple levels of proof automation. In this chapter, those custom tactics are presented.

For a brief introduction to this topic, you can have a look at this section of the talk about MRiscX at Lean Together 2026.

4.1. Custom Tactics🔗

🔗tactic
sapply_s_seq

Apply the Hoare rule S_SEQ in order to split the current Hoare triple into two. To do so, the names and values must be provided explicitly, each separated by a colon.

The order is:

  1. P

  2. R

  3. L_W

  4. L_W'

  5. L_B

  6. L_B'

Also, try to automatically solve most of the "side goals" that are generated during the process. These side goals are generally statements about the provided sets (e.g., L_W ≠ ∅), which are trivial in most cases.

The same tactic can be used without providing P

🔗tactic
sapply_s_seq''

Like sapply_s_seq, but without solving the sidegoal L_b = L_b' ∩ L_b''.

🔗tactic
auto_seq

Apply S_SEQ to 'peel' off the last instruction. Also, try to solve all goals which are created during the process except for the two goals, which involve the actual Hoare-triples which will be generated.

🔗tactic
apply_spec

Apply a given specification and try to get rid of all proof goals which are create during the process.

To be able to apply a specification, L_B must contain every line except the one that is being executed. For example, if you want to apply the specification for the Instr.LoadImmediate, which is on line l, and you have some (P Q : Prop), then the Hoare-triple needs to look like this:

⦃P⦄ l ↦ ⟨{l+1} | {n:UInt64 | n ≠ l + 1}⟩ ⦃Q⦄

TODO: Avoid having to provide pc, registers and values in application of specification

4.2. General Idea in a Proof🔗

The general idea of a proof of the formal correctness of an implementation looks like this:

  1. Identify:

    1. Sequential code sections

    2. Conditional branches

    3. Loops

  2. Use the tactic S_SEQ (or the custom tactic sapply_s_seq) to isolate these sections.

  3. These situations might come up:

    1. Sequential code sections

      • Use S_SEQ or some custom tactic (e.g. auto_seq) to "peel off" the last instruction and inspect it in isolation. You might have to think of an appropriate R.

      • Use the specification for the isolated instruction to formally verify the correctness of this single step.

      • Repeat the process.

    2. Conditional branches

      • Apply S_COND

      • Show that Q is valid with

        1. P \wedge C

        2. P \wedge \neg C by going through both code sections and repeating from step 1.

    3. Loops

      • Apply S_LOOP by finding the condition C of the loop, the loop invariant I, and the loop variant V as described in the introduction to S-LOOP

      • Show the formal correctness of the loop body when C is true (the condition for one loop iteration holds)

      • Show that the loop is exited when ¬C (the condition for another loop iteration does not hold)

For some easy examples, have a look at the Example file. There you can find how the custom tactics are applied to some small code examples.

A larger example can be seen in the file OtpProof. Here, an implementation of the "One-Time-Pad" was formally verified. Note that this example is quite old and should be refactored.