C0deine is a reference compiler for c0. It is written in Lean 4, which allows us to express the formal semantics in the same language as the compiler itself. You can try it out in your browser at theabrick.com/c0!
Currently, we only support targeting WebAssembly. In the future, we hope to also target C, x86-64 assembly, and potentially C0 bytecode. No phases of the compiler are currently proven correct, but we are hoping to do so in the future.
Information about the source languages and standard libraries can be found in langs.
This project requires Lean4. The example programs that evaluate the compiled code requires node.
To compile C0deine run:
lake exe cache get
lake buildIf you'd like to compile C0deine itself to WebAssembly this requires emscripten. Once installed run the following commands:
lake build wasm_builder
lake exe wasm_builderThis can take some time. Once finished, the compiler can then be invoked
via lake run js <args> or node ./.lake/build/wasm/main.js <args>. To compile
to WASM that can be used without node, run lake exe wasm_builder web.
Run bin/c0c -h to verify everything compiled correct and to see the help
message. By default, C0deine targets the WebAssembly Text Format (WAT). It also
can target the WebAssembly Binary Format (WASM).
The file example.js provides a small example how to
evaluate a program (it also compiles it using compile.sh).
To run the example driver, cd testing and run node example.js <test>. To
compile, execute (if applicable), and verify the result
./run.sh <test/test_dir> can be used.
The C0deine compiler depends on a number of other packages that are also being maintained. Here is a list of them:
- Numbers -- Arbitrary bit-length signed integers in Lean (following the WebAssembly specification).
- Lean-Wasm -- Formalisation of the WebAssembly specification as well as other related utilities.
- Control Flow -- Theorems about control flow graphs as well as implementations of various utilities.
- Lean2Wasm -- A tool for compiling Lean source code into WebAssembly.
- c0_web_driver -- A web-based UI for both compiling c0 code and executing it in the browser.
Issues and PR are always welcome! This is a very large project and although I've already done a lot, there's much more I'd love to do! Even if you don't have much (if any) experience with writing Lean you can still help. If you are interested or have any questions feel free to DM me (Thea Brick) on the Lean Community Zulip.
Special thanks to @JamesGallicchio for their initial implementation of the parser and other core utilities used by the compiler.
"c0deine" is a reference to the major component of a street drug sometimes called "lean" (see, e.g., here). The pun was hard to resist.
That said, opioid addiction is not a joke, and codeine is still one of the most commonly abused opioids. please reach out if the name makes you uncomfortable (we can change it).