MRiscX

KO | EN

gitlite — search

#python #java #python3 #arduino #golang #machine-learning #rust #html #flask #javascript #seismology #nodejs

★ 22 Open GitHub ↗

A certified RISC-V Interpreter with Hoare-logic in Lean

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

# MRiscX

MRiscX aims to provide a low-threshold introduction to the world of formal methods.
To this end, an environment has been developed that allows RISC-V assembly code to be verified in 
Lean using Hoare logic.

Please keep in mind, this project is still in development and far from finished. 
For any problems and issues you encounter while using this library, I 
would be happy if you report them!

For more information about this project and how to use it, have a look into the 
[documentation](https://docs.mriscx.dev)

## Installation

The project is dependent on mathlib. If mathlib is not present, it will be installed to your project 
automatically after adding this project as a dependency.

Add this project to your lakefile.toml like this

```toml
[[require]]
name = "MRiscX"
git = "git@github.com:JulsDE/MRiscX.git"
rev = "main"
version = "0.1.0-v4.33.0"
```
Then, execute 
```bash
lake update 
```
in your project. When finished successfully, restart the `Lean Language Server`  and import
```lean4
import MRiscX.Basic
``` 
into a `.lean` file. After a final `Restart File` you can start using the library.

## Verify your own code

To perform a proof of correctness, you can create a new file, import
```lean4
import MRiscX.Basic
```

and start by defining the Hoare triple.

In general, a Hoare triple in MRiscX looks like this: 
```lean4
example (r₁ r₂ r₃ v₁ v₂ : UInt64)
        (P Q : Prop) (l : UInt64)
        (L_W L_B : Set UInt64):
  mriscx
    main:
          li x r₁, v₂
          li x r₂, v₂
          xor x r₃, x r₁, x r₂
          j _store

_some_label:
          addi x r₁, x 0, 42
  end
  ⦃P⦄ l ↦ ⟨L_W | L_B⟩ ⦃Q⦄
  := by sorry
```

A concrete example of a code snippet which can be verified: 
```lean4
example:
    mriscx
      first:  li x 0, 2
              li x 1, 0
              la x 2, 0x123
    end
    ⦃¬⸨terminated⸩ ∧ x[4] = 123⦄
    "first" ↦ ⟨{3} | ({n:UInt64 | n = "first"} ∪ {n:UInt64 | n > 3})⟩
    ⦃(x[0] = 2 ∧ x[1] = 0 ∧ x[2] = 0x123 ∧ x[4] = 123) ∧ ¬⸨terminated⸩⦄
  := by sorry
```
As you can see, it is possible to use labelnames as indicator where the programcounter should 
start / finish.

For more examples and explanations, have a look into files inside the 
[example folder](MRiscX/Examples), especially the file 
[`Examples.lean`](MRiscX/Examples/Examples.lean) might be helpful.

**_NOTE:_** In the current version, it is necessary to put the preconditions and postconditions in parentheses, with the exception of `¬⸨terminated⸩` (e.G. 
⦃**(** x[0] = ∧ x[1] = 1 **)** ∧ ¬⸨terminated⸩⦄), in order to successfully apply the 
specification.

## Structure of the project
- `MRiscX/`
  Contains all relevant Lean files of the project.

- `MRiscX/Basic.lean`
  Imports all relevant Lean files of the project. By importing this file once, all necessary files 
    are imported so that Hoare triples can be formulated.

- `MRiscX/AbstractSyntax`
  Contains all the abstract syntax objects the assembly language essentially bases on

- `MRiscX/Delab`
  Contains the files responsible for delaboration of assembly language and Hoare triple

- `MRiscX/Elab`
  Contains the files handling the elaboration and some specific expr processing

- `MRiscX/Util`
  Contains some Utility functions like theorems about sets or UInt64 used several times

- `MRiscX/Hoare`
  Contains all the files about the Hoare logic and Hoare triples

- `MRiscX/Hoare/HoareAssignmentElab.lean`
    Contains the function 
    `replaceKeywords`, which translates the tokens into corresponding function calls.

- `MRiscX/Hoare/HoareCore.lean`
    Definition of the central functions `weak` and `hoare_triple_up`.

- `MRiscX/Hoare/HoareRules.lean`
    Formalization of Hoare rules and their associated proofs.

- `MRiscX/Parser/`
  Contains the syntax definitions of the assembly language and Hoare triples

- `MRiscX/Semantics/`
  Contains files about the semantics of the assembly language 
  
  - `MRiscX/Semantics/Run.lean`
    Contains the `MState.runOneStep` and `MState.runNSteps` functions.

- `MRiscX/Semantics/MsTheory.lean`
    Contains basic theorems about properties of machine states.

- `MRiscX/Tactics/`
    Contains all the custom tactics.

- `MRiscX/Tactics/SplitLastSeq.lean` 
    Contains the logic behind the tactic `auto_seq`, which tries to 
    "peel off" the last instruction with applying `S-SEQ` and calculating all the missing values.
  
  - `MRiscX/Tactics/CodeProofTactics.lean` 
    Contains various proof tactics to automate the process of verifying the formal correctness of 
    a program

- `MRiscX/Examples/`
  Contains some working examples

- `MRiscX/Examples/Examples.lean`
    Contains many small examples of Hoare-triples which are verifiable on correctness pretty easily.

- `MRiscX/Examples/OtpProof.lean`
    Contains a complete proof of correctness of an implementation of the One-Time-Pad. Individual steps are outsourced to 
    `MRiscX/Examples/singleProofsOTP.lean`.

## Known issues
- In the current version, it is necessary to put the preconditions and postconditions in 
  parentheses, with the exception of `¬⸨terminated⸩` (e.G. 
  ⦃**(** x[0] = ∧ x[1] = 1 **)** ∧ ¬⸨terminated⸩⦄), in order to successfully apply the 
  specification. 
- The `auto_seq` tactic currrently does **not** work.

MRiscX

Explore Similar Repositories

Was this content helpful?

Recent Feedback

Download README