How can I manually compile the emitted c-code to riscv?

Stream: general

[Felix Wilking]

I have a graduate independent study project involving proving code to be run as an OS kernel on a simulated risc-v processor, and I'm currently considering lean as a proof assistant (I'd also appreciate input on this usecase).

Therefore I need to be able to compile lean code to rv64.
Right now I'm just trying to figure out how to manually compile the emitted code to my native x86 binary using the following command.
gcc -I~/elan/toolchains/leanprover--lean4---stable/include/ Main.c
I also tried with clang, and I'm getting a lot of errors complaining that various macros are not defined.

[Henrik Böving]

You can get there with what is described here https://kuruczgy.com/blog/2024/07/31/lean-esp32/ but this still relies on a lot of C code in libc and libc++ just to get the runtime working. Lean is also not generally something that people would write a real operating system in given that it is not at all a systems programming language.

I would suggest to use proof techniques like differential fuzzing instead of trying to run Lean code directly.

[Felix Wilking]

Henrik Böving said:

What proof assistant would you recommend? I've been considering idris, but I know CoQ and isabelle are more commonly used. But the PA needs to emit RISC-V binary and my understanding is isabelle cannot do that.

[Henrik Böving]

Why would the proof assistant need to emit a RISC-V binary? There are plenty of ways to verify code without the proof assistant emitting the binary really.

[Felix Wilking]

my goal is to first write an intermediary stack based language and then write the OS in that language.

[Henrik Böving]

If you are implementing your own programming language you'd want to implement a compiler as well instead of using the code generation facilities of whatever language wouldn't you? Also note that none of Idris, Coq or Isabelle are capable of producing binaries that run on bare metal.

[Henrik Böving]

My recommended approach for this project would be to implement your OS in a proper systems language like Rust and then implement a model in Lean or some other proof assistant and differentially fuzz a compiled version of that model against your OS implementation. This is e.g. the technique used by https://www.kernkonzept.com/ to verify L4re.

You can also use the techniques used by Isabelle to verify seL4 which would include first implementing your OS in C and then doing proofs about the C directly. That's going to give you some more certainty in the correctness of your proof but increase the effort quite drastically.

In general implementing something that resembles an OS on RISC-V is probably already challenging enough for most student projects. Unless you really know what you are doing on the RISC-V end already and have a significant amount of time over a significant time period for this project

[Felix Wilking]

what do you mean by run on bare metal? Do you mean without environmental overhead like a garbage collector? In my research it seems like idris is capable of compiling its racket backend to risc-v, but that might contain some runtime environment or something, I'm not sure.
As for implementing an OS, I've already taken a rigorous undergraduate OS class and did very well, and I'm currently taking a graduate level one as well, so I think it's doable, but maybe I'm mistaken.
The reason I had the idea to create the intermediate language was because it seemed like it would be a very useful crossroads between ease of development and ease of verification.

[Henrik Böving]

All of those languages usually require a runtime to manage their memory indeed. Maybe there is some trick involved though I don't know about that.

Implementing an operating system while knowing how it works in theory from a class is still an additional bump in complexity. You'll be spending most of your time reading the RISCV manual that describes privileged execution etc.

If you have never implemented OS level functionality like setting up a page table or an allocator just writing the OS is going to be hard in its own right. I still don't know how much time you have but if you are seriously considering it I would recommend the differential fuzzing approach at most. If not just implementing an OS without versification.