Stream: lean4

Topic: System programming using Lean 4

Ryan Lahfa (Feb 05 2021 at 01:24):

For school reasons, I am looking to make a (micro|uni)-kernel in some language supporting formal verification, I know some Lean 3 and I was wondering if it was a good idea to jump into Lean 4 and try to make it into Lean 4, it looks like it might be able to fit the bill, I wonder how feasible this is?

e.g. how much stuff has to be reimplemented in baremetal to kickstart Lean 4 programs without any operating system on x86_64 for example? Is it easy or like insanely difficult?

Ryan Lahfa (Feb 05 2021 at 01:25):

I know the existence of stuff like https://github.com/stepcut/idrOS and am ready to carry out similar stuff if required

Mario Carneiro (Feb 05 2021 at 01:25):

There are commands that let you write bindings to C calls, so as long as C can do it I think it's possible to make lean do it

Mario Carneiro (Feb 05 2021 at 01:25):

I'm not sure how include files work though

Ryan Lahfa (Feb 05 2021 at 01:27):

I can indeed write down the required stuff to provide primitives in C, then if I can call them from Lean world and write down a model of they should work (which would be really cool if it stops at some boundary to define)

Also, maybe harder question, can Lean 4 compile to non-x86_64 platforms, e.g. RISC-V or ARM?

Mario Carneiro (Feb 05 2021 at 01:27):

If lean.h doesn't work because the baremetal environment doesn't have the support this might be a trickier task though. In particular I can imagine memory allocation being a sticking point

Mario Carneiro (Feb 05 2021 at 01:27):

lean compiles to C which compiles via any C compiler. So yes, it should work on any arch

Ryan Lahfa (Feb 05 2021 at 01:28):

Mario Carneiro said:

lean compiles to C which compiles via any C compiler. So yes, it should work on any arch

Wow! That's really neat :>

Ryan Lahfa (Feb 05 2021 at 01:34):

Hm, it looks like that I would need to patch this: https://github.com/leanprover/lean4/blob/master/src/runtime/object.cpp and everything else would reuse those implementations but I might be wrong?

Mario Carneiro (Feb 05 2021 at 01:35):

wait, that's C++ code? I thought the runtime was all C

Ryan Lahfa (Feb 05 2021 at 01:36):

Well, it is ; but as it looks like to be wrapped in some FFI, I imagine that I can just replace the cool STL containers & stuff by baremetal ol'C

Ryan Lahfa (Feb 05 2021 at 01:37):

I wonder if I can do unikernels of Lean 4 programs :D

Wojciech Nawrocki (Feb 05 2021 at 02:31):

@Ryan Lahfa I do not wish to discourage you, by all means do try to put Lean on bare metal! But it does seem like a Lean 4 OS would be a work-intensive project. While it is true that Lean programs compile to C which you could then compile to any architecture, they also link against the language runtime. So while you can definitely compile to RISC-V or ARM (with some obvious rough edges, but nothing should be fundamentally difficult), this is RISC-V or ARM with an OS. Being a reference-counted language, Lean needs the allocator in its runtime to function. So as Mario mentioned, you would need a heap, which is quite a few chapters into "Writing an OS in Rust". By contrast, there is an allocation-less subset of Rust which is used in that guide to get off the ground fairly quickly with displaying some text into VGA. On top of all this, numerical Lean code uses libgmp providing which in real mode sounds.. challenging. It sounds like you would have to cut that out of the runtime also. While I know nothing about Idris internals, looking at the idrOS project you linked it seems its author has written about 9k lines of C and 9 lines of Idris and then given up, so make of that what you will. Having said all this, I think it should be possible, it might just require a fairly high level of determination.

Calvin Lee (Feb 05 2021 at 04:28):

Wojciech Nawrocki @Ryan Lahfa Very much agree, having written an OS in Rust. I've been thinking about this idea a lot too. There are many parts of a kernel where heap allocation really shouldn't happen, or where data must be placed in certain places. Doing a unikernel should be a lot easier IMO, since you could write the whole runtime/OS in C/Rust and then use it in Lean.
Maybe if there were a way to make the typechecker linear so allocation wouldn't be necessary this could work.

Calvin Lee (Feb 05 2021 at 04:33):

Another issue I think you'd run into here is stack space.
Operating systems have notoriously tiny stacks (in some places, like the kernel stack for a process), usually just one page.
I know some OSdevs who have long, recursive functions, and if they recurse too much they have to be offloaded into new threads as to not overflow the stack. Really the rule of thumb is to never have your callstack over 5 layers deep.
On the other hand, I've had __huge__ issues with lean recursing too much. I've started to compile the program I'm writing with LEANC_OPTS="-fsplit-stack " so it can't overflow... and obviously this isn't possible in an OS context.

Ryan Lahfa (Feb 05 2021 at 12:14):

@Wojciech Nawrocki @Calvin Lee Well, it definitely makes sense to me ; I'm just wondering what is the shortest path to get something like a unikernel for example and what properties could I get from writing the rest in Lean 4, etc.
That's more an experiment than something else, my fallback project being writing the project in Rust with some design by contracts lib.

Joe Hendrix (Feb 06 2021 at 02:11):

@Ryan Lahfa An OS in Lean 4 sounds awesome. A practical consideration that Wojciech also mentioned is the Lean runtime is still pretty big. In particular it depends on GMP, and it introduces a bunch of dependencies due to the way constants are compiled. Essentially, you end up pulling a lot of the definitions needed for implementing Lean in the runtime dependencies.
We've gotten Lean 4 programs compiling and running as a process on a Rasberry Pi, but I think a more resource constrained environment would be a lot of work. Leo has heard about our experience at Galois, but I don't know how much of a priority it is to minimize the runtime and enable more bare-metal applications. I'd like to be able to compile Lean 4 code to Arduino eventually.

Leonardo de Moura (Feb 06 2021 at 19:04):

@Joe Hendrix We are currently fixing bugs and writing papers, but we hope to get back to the compiler in April. This issue is a priority.

Christian Pehle (Feb 11 2021 at 18:10):

I would distinguish between writing an OS and getting C++ to run on bare metal. The latter is relatively easy to do if you have a reasonably powerful embedded system as a target. All you need to get started is a bare metal build of gcc, an embedded C library like https://sourceware.org/newlib/, a linker script and a small set of c++ specific assembly routines. You need surprisingly little to get C++ running, see for example https://github.com/electronicvisions/libnux/blob/master/src/crt.s. So before trying your hand at compiling lean, I would start out just setting up an environment that allows you to compile C++ to bare metal on the platform of your choice.

Ryan Lahfa (Feb 11 2021 at 19:10):

We already done such things on RISC-V and FPGAs, so that's why we're interested into the next steps

Last updated: May 07 2021 at 13:21 UTC