Divine Intellect Compiler

🪄 Dependently typed toy language with holes developed in rust for HackSheffield 9! Developed using Rust, Larlpop and Z3!

View Devpost · Report Bug · Request Feature

The Divine Intellect Compiler brings together dependently typed programming and large language models (LLMs) in an experimental way. The compiler uses a toy language called Divinity, where developers can write programs with holes (placeholders) for incomplete code. These holes can then be filled in automatically by an integrated LLM, then verified (proved!).

The key feature of Divine Intellect is its ability to verify that the code generated by the LLM is correct. Using dependent types and satisfiability checking, the compiler ensures that any LLM-generated code adheres to the constraints you define. For instance, you can create a BoundedInt type to enforce that values must always fall within a specific range.

By combining LLM support with formal verification, the Divine Intellect Compiler allows you to generate code while making sure it meets the necessary requirements and constraints, offering an extra level of assurance that the code is working as expected.

Infact, the Divine Intellect Compiler is inspired by Terry Davis' famous TempleOS system, and surrounding projects such as HolyC, but with a verification twist.

(back to top)

High Level Compiler Overview

Divine Intellect Compiler, uses lalrpop, a lightweight language for defining grammars in a concise, declarative style, which builds a parser distinct for the given context-free-grammar. Here's an example of one rule, others can be found in src/calculator1.lalrpop.

pub FunctionDefinition : Block = {
    "fn" <id: IDString> "(" <args: Comma<TypedArgument>> ")" "->" <ret_type: IDString> "{" <stmts: Semicolon<Statement>> "}" => {
        Block::FunctionDefinition(id, args, ret_type, stmts)
    }
}

After we have obtained the program in it's AST form, we can verify this using Z3 Theorem Prover. Firstly, we perform a Static Singular Assignment (SSA) transform, before we encode the program into Z3 and check it's satisfiability.

• Types are given as expressions, i.e. σ > 10
• Since Z3 checks satisfiability, the complement is encoded, i.e. σ ≤ 10
• We prove the unsatisfiability of the complement, and the satisfiability of the type to prove correctness.

The AST is then interpreted directly using a bespoke interpreter written in Rust. This can be found in src/compile/interpreter.rs, and supports I/O using show and getint commands.

(back to top)

Since the project was born out of a 24-hour hackathon, there are going to be issues and bugs - note the lack of installation guidance here as an example. If you wish to contribute to Divine Intellect Compiler or Divinity, please feel free to create a feature branch or raise an issue! If you encounter any big issues, or get really stuck - feel free to contact whoever you think is most relevant to the issue you are encountering.

1. Fork the Project
2. Create your Feature Branch (git checkout -b feature/AmazingFeature)
3. Commit your Changes (git commit -m 'Add some AmazingFeature')
4. Push to the Branch (git push origin feature/AmazingFeature)
5. Open a Pull Request

(back to top)

Distributed under the MIT License. See LICENSE.txt for more information.

(back to top)

Amber Swarbrick - Compiler Implementation Toby Clark - Verification Algorithm Implementation