Basic file reading plugin infrastructure set up

[blainehansen]

Hello!

Today I managed to get a little proof of concept working, one that lays a simple foundation for the first intended phase of the project. The ocaml code in plugins creates a coq plugin that can read from source files and use the contents to create coq definitions. If you look at theory/test.v you can see the Magmide command being used, as it reads from something.mg and uses the contents to create a coq expression defined under the name yo, which you can then prove things about. Run dune build to compile the project.

Magmide "something.mg" use yo.
Theorem yo_true: yo = true.
Proof. reflexivity. Qed.

The goal here is to allow magmide source code to be parsed from files and ingested into Coq to prove things about functions. The final version of the plugin will likely accept multiple identifiers after the use to ingest multiple functions from the same file, and of course all the parsing and transformation is completely undone.

The next bit of plumbing work is figuring out a rust program that can accept the parsed syntax trees and emit llvm from them. Just figuring out the plumbing is all that we need, the llvm generated doesn't have to be interesting, but we do need the ability to inspect/walk the parsed ast. It might make sense to do the parsing with rust, but in general we should avoid transforming back and forth between different syntax trees, and since in order to prove things about the ast in Coq it has to be representable as ocaml values, then even if the parsing is done in rust it should produce ocaml values.
https://docs.rs/ocaml/latest/ocaml/
https://github.com/TheDan64/inkwell

Here are the guides I used to get my ocaml/opam/dune/coq environment set up. Watch out for opam switches, I wasted a lot of time reinstalling packages twice after accidentally switching to an old version of ocaml.
https://opam.ocaml.org/doc/Install.html
https://ocaml.org/docs/install.html
https://coq.inria.fr/opam-using.html

[remimimimimi]

Maybe we should only do this with Coq and OCaml, because OCaml already has good bindings for LLVM, and thus we can verify our OCaml code (https://foobar-land.github.io/coq-of-ocaml/)? Also, I don't think that writing the Coq plugin is a good idea, I suppose that this is an overcomplication. Therefore, the solution from #10 is different from the plugin example.

[blainehansen]

I'm glad you pushed back, because there are a few paths forward.

First, in regards to making a coq plugin vs transpiling code to coq files, I'm definitely not a fan of just transpiling into coq files. It's a lot messier, and honestly just adds clutter and complexity since instead of just creating an immediate in-memory ast to give directly to coq, we have to go through all the hassle of outputting an ast to files and ensuring we're doing so correctly. If someone wants to inspect the magmide structures, there's always coq's Print command, and we can still choose to create a coq notatation to make them easier to look at. I've already done the pretty painful work of figuring out how to make the plugin and which coq ast to construct (I'm using the concrete syntax type, which means it will be a lot easier and more intuitive to build than a more raw internal abstract one), so the truly high friction part is already behind us.

Then, rust vs ocaml. We need to build a parser and an llvm builder somehow. Either of them could be in ocaml or rust, although it seems easier and better supported to call rust from ocaml than the other way around. Here's a bunch of thoughts about why I'm leaning toward rust even after I earlier said I wanted to use Coq for everything:

• Rust has better libraries and communities for these tasks. Ocaml's LLVM bindings are literally just direct exposures of the fairly obtuse C api. Inkwell in contrast is much cleaner and much better documented.
• The goal of Magmide is to make verification of imperative programs better. It's about being able to create bare metal, zero runtime, truly computational programs. Host Magmide will be a lot like rust or C. It seems more realistic to build as much of the pipeline with a language with a similar structure and a more amenable culture and goals, rather than leaning harder into the more academic culture.
• As soon as we're capable of compiling Magmide code into LLVM, then we'll be able to integrate that Magmide into any other language. It will be easier to verify little tiny pieces of Magmide and then integrate them into a largely rust pipeline than it would be to integrate them into a largely ocaml pipeline.
• We'll get everything all verified, but no matter what we have to be patient about that, since so many parts of this pipeline will be so complicated to verify. For now I just want to get something working. Even if we did this in Coq/ocaml, we'd likely write the code "quick and dirty" and verify it later, so using rust instead allows that process to be more pleasant and aligns more with the intended final destination of the project.

The real dream of this project is to escape from Coq and languages like it, and build something as powerful that isn't as bogged down in an impractical academic culture. I'd rather use Coq as little as possible, only using it for the single thing it's truly useful for, and then replace it with a Host Magmide proof checker as soon as possible.

[jeremyschlatter]

The next bit of plumbing work is figuring out a rust program that can accept the parsed syntax trees and emit llvm from them.

I've been working on this. I have a tiny bit of rust that does both parsing from text to syntax trees and rendering from syntax trees to llvm. I have enough plumbing working to check the trees in coq, currently working on plumbing to add coq vernacular to trigger the rendering. Hopefully will have it in good enough shape to send a PR in a week or two. Here's my development branch: https://github.com/jeremyschlatter/magmide/tree/parser

[blainehansen]

This is awesome! 👏
I looked through your branch and it seems you've added the skeleton of basically everything I talked about and now just need to clean it up! :) Is that accurate? I'm a bit confused about what you mean by "add coq vernacular to trigger the rendering".

It seems this line ought to correctly construct an Instruction value by calling your hello function, right? (I haven't had a chance to pull down your code and try it)

MagmideParse "%0 = 2 + 2" as four.

I'd love it if you made a draft pull request so I can see what you've added, and perhaps I can jump in to help you finish it off :)

I need to start figuring out the real theory and design so we can actually start pushing toward something useful! The work you've done here would largely exhaust the scoped next steps ha.

[jeremyschlatter]

Here's the draft PR :)

I responded to your questions there.

[blainehansen]

@jeremyschlatter, I noticed you work at MIRI. I'm interested in EA, and participate in/help run the local EA group in my city. Nice to see a fellow concerned citizen :)
I'm curious, is your interest in Magmide related to your work at MIRI? Or are you just personally interested in logic and verification?

[jeremyschlatter]

Nice! :)

My interest in Magmide is mostly personal. Though I do think a great version of Magmide could be helpful to MIRI, as it could be helpful to lots of causes.