Implement proper Lean emission (#1)

This commit takes the sketchy code that was already on the branch and
turns it into a proper flexible structure for the emission of Lean code.
It also separates the CLI from the emission library, allowing the tool
to be more flexible.

Please note that this is still a work in progress, and not every feature
of Noir is supported as of yet.

Cargo.toml

@@ -3,11 +3,30 @@ name = "lampe"
 version = "0.1.0"
 edition = "2021"
 
-# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+description = "A tool for extracting Noir programs to equivalent definitions in Lean."
+categories = ["compilers", "command-line-utilities"]
+keywords = ["compiler", "transpiler", "lean", "noir"]
+
+repository = "https://github.com/reilabs/lampe"
+license = "MIT"
 
 [dependencies]
+fm = { path = "../noir/compiler/fm" }
+nargo = { path = "../noir/tooling/nargo" }
 noirc_driver = { path = "../noir/compiler/noirc_driver" }
+noirc_errors = { path = "../noir/compiler/noirc_errors" }
 noirc_frontend = { path = "../noir/compiler/noirc_frontend" }
-nargo = { path = "../noir/tooling/nargo" }
 
-itertools = "0.12.1"
+clap = { version = "4.5.17", features = ["unstable-v5"] }
+derivative = "2.2.0"
+indoc = "2.0.5"
+itertools = "0.13.0"
+log = "0.4.22"
+thiserror = "1.0.63"
+
+[dev-dependencies]
+anyhow = "1.0.87"
+
+[[bin]]
+name = "cli"
+path = "src/bin/main.rs"

README.md

@@ -0,0 +1,17 @@
+# Lampe
+
+> Lampe (/lɑ̃p/), a light to illuminate the darkness
+
+This project contains a model of [Noir's](https://noir-lang.org) semantics in the
+[Lean](https://lean-lang.org) programming language and theorem prover. The aim is to support the
+formal verification of both the Noir language semantics and the properties of programs written in
+Noir.
+
+## Building
+
+In order to build this you will need to clone the Reilabs [fork](https://github.com/reilabs/noir) of
+the Noir repo next to the clone of this repo. In other words, if you have this repository at
+`reilabs/lampe`, then that fork needs to be at `reilabs/noir`. You will also need to check out the
+`lampe` branch in the `noir` repo. This will allow the Rust project to build.
+
+The Lean project should build on its own.

rustfmt.toml

@@ -0,0 +1,56 @@
+# This file contains the configuration for the ecosystem's formatting tool, `rustfmt`. It only contains entries where
+# they differ from the default or for unstable attributes whose default may change.
+#
+# For more information on the configuration see here: https://github.com/rust-lang/rustfmt/blob/master/Configurations.md
+
+# High-level configuration, telling rustfmt which featureset to use.
+edition = "2021"
+version = "Two"
+
+# Configuration controlling general code style.
+brace_style = "SameLineWhere"
+chain_width = 70
+combine_control_expr = true
+condense_wildcard_suffixes = true
+control_brace_style = "AlwaysSameLine"
+empty_item_single_line = true
+enum_discrim_align_threshold = 20
+fn_single_line = false
+force_multiline_blocks = false
+format_strings = true
+hex_literal_case = "Lower"
+indent_style = "Block"
+inline_attribute_width = 0
+match_arm_blocks = true
+reorder_impl_items = true
+single_line_let_else_max_width = 70
+space_after_colon = true
+spaces_around_ranges = false
+struct_field_align_threshold = 20
+struct_lit_single_line = true
+struct_variant_width = 70
+trailing_comma = "Vertical"
+trailing_semicolon = true
+type_punctuation_density = "Wide"
+use_field_init_shorthand = true
+where_single_line = false
+
+# Configuration controlling the formatting of macros.
+format_macro_bodies = true
+format_macro_matchers = true
+
+# Configuration controlling how imports are formatted.
+group_imports = "StdExternalCrate"
+imports_granularity = "Crate"
+imports_layout = "HorizontalVertical"
+
+# Configuration controlling how spacing is formatted.
+blank_lines_lower_bound = 0
+blank_lines_upper_bound = 1
+
+# Configuration controlling the formatting of comments.
+comment_width = 80
+format_code_in_doc_comments = true
+normalize_comments = true
+normalize_doc_attributes = true
+wrap_comments = true

src/bin/main.rs

@@ -0,0 +1,79 @@
+//! A utility for extracting [Noir](https://noir-lang.org) programs to
+//! equivalent definitions in the [Lean](https://lean-lang.org) theorem prover
+//! and programming language.
+//!
+//! # Limitations
+//!
+//! It currently only supports single-file programs, pending further expansion
+//! to support full Noir projects. The stdlib functions properly at this stage.
+
+#![warn(clippy::all, clippy::cargo, clippy::pedantic)]
+
+use std::{fs::File, io::Write, path::PathBuf, process::ExitCode};
+
+use clap::{arg, Parser};
+use lampe::{noir::source::Source, noir_to_lean, Project, Result};
+
+/// The default Noir project path for the CLI to extract from.
+const DEFAULT_NOIR_PROJECT_PATH: &str = "";
+
+/// The default Noir filename for the CLI to extract from.
+const DEFAULT_NOIR_FILE_NAME: &str = "main.nr";
+
+/// The default output file for the generated definitions.
+const DEFAULT_OUT_FILE_NAME: &str = "Main.lean";
+
+/// A utility to extract Noir code to Lean in order to enable the formal
+/// verification of Noir programs.
+#[derive(Clone, Debug, Parser)]
+pub struct ProgramOptions {
+    /// The root of the Noir project to extract.
+    #[arg(long, value_name = "PATH", default_value = DEFAULT_NOIR_PROJECT_PATH)]
+    pub root: PathBuf,
+
+    /// The specific file in the Noir project to extract.
+    #[arg(long, value_name = "FILE", default_value = DEFAULT_NOIR_FILE_NAME)]
+    pub file: PathBuf,
+
+    /// The file to output the generated Lean sources to.
+    #[arg(long, value_name = "FILE", default_value = DEFAULT_OUT_FILE_NAME)]
+    pub out_file: PathBuf,
+}
+
+/// The main function for the CLI utility, responsible for parsing program
+/// options and handing them off to the actual execution of the tool.
+fn main() -> ExitCode {
+    // Parse args and hand-off immediately.
+    let args = ProgramOptions::parse();
+    run(&args).unwrap_or_else(|err| {
+        eprintln!("Error Encountered: {err}");
+        ExitCode::FAILURE
+    })
+}
+
+/// The main execution of the CLI utility. Should be called directly from the
+/// `main` function of the application.
+///
+/// # Errors
+///
+/// - [`Error`] if the extraction process fails for any reason.
+pub fn run(args: &ProgramOptions) -> Result<ExitCode> {
+    let source = Source::read(&args.file)?;
+    let project = Project::new(&args.root, source);
+
+    let emit_result = noir_to_lean(project)?;
+    if emit_result.has_warnings() {
+        for warning in &emit_result.warnings {
+            println!("{warning:?}");
+        }
+    }
+
+    let lean_source = emit_result.take();
+    let mut out_file = File::open(&args.out_file)
+        .map_err(|_| lampe::error::file::Error::MissingFile(args.out_file.clone()))?;
+    out_file
+        .write(lean_source.as_bytes())
+        .map_err(|_| lampe::error::file::Error::MissingFile(args.out_file.clone()))?;
+
+    Ok(ExitCode::SUCCESS)
+}

src/error/compilation.rs

@@ -0,0 +1,23 @@
+//! Errors to do with compilation of Noir.
+
+use noirc_driver::ErrorsAndWarnings;
+use thiserror::Error;
+
+/// The result type for dealing with compilation-related errors.
+pub type Result<T> = std::result::Result<T, Error>;
+
+/// Errors for compilation of Noir source code.
+#[derive(Debug, Error)]
+pub enum Error {
+    #[error("Could not successfully check crate:\n{diagnostics:?}")]
+    CheckFailure { diagnostics: ErrorsAndWarnings },
+
+    #[error("Noir Error: {_0}")]
+    Other(String),
+}
+
+impl From<ErrorsAndWarnings> for Error {
+    fn from(diagnostics: ErrorsAndWarnings) -> Self {
+        Error::CheckFailure { diagnostics }
+    }
+}

src/error/emit.rs

@@ -0,0 +1,16 @@
+//! Errors from the emit phase of the library.
+
+use thiserror::Error;
+
+/// The result type for dealing with emit-related errors.
+pub type Result<T> = std::result::Result<T, Error>;
+
+/// Errors during the emission of Lean from Noir source code.
+#[derive(Debug, Error, PartialEq)]
+pub enum Error {
+    #[error("Could not extract identifier from {_0}")]
+    MissingIdentifier(String),
+
+    #[error("Indentation level cannot be decreased below zero")]
+    CannotDecreaseIndentLevel,
+}

src/error/file.rs

@@ -0,0 +1,21 @@
+//! Errors to do with handling files.
+
+use std::path::PathBuf;
+
+use thiserror::Error;
+
+/// The result type for dealing with file-related errors.
+pub type Result<T> = std::result::Result<T, Error>;
+
+/// Errors for handling files when interacting with the Noir compiler driver.
+#[derive(Debug, Error)]
+pub enum Error {
+    #[error("Could not read file at {_0:?}")]
+    MissingFile(PathBuf),
+
+    #[error("File at {_0:?} already exists in the project")]
+    DuplicateFile(PathBuf),
+
+    #[error("Noir Error: {_0}")]
+    Other(String),
+}

src/error/mod.rs

@@ -0,0 +1,30 @@
+//! The error types for use at the boundary of the library.
+
+pub mod compilation;
+pub mod emit;
+pub mod file;
+
+use thiserror::Error;
+
+/// The result type for use at the boundary of the library.
+pub type Result<T> = std::result::Result<T, Error>;
+
+/// The top-level error type for use at the boundary of the library.
+///
+/// It provides conversions from the more-specific internal error types to ease
+/// usage, while also ensuring a strongly-typed error boundary to enable proper
+/// handling.
+#[derive(Debug, Error)]
+pub enum Error {
+    /// Errors in compilation.
+    #[error(transparent)]
+    Compile(#[from] compilation::Error),
+
+    /// Errors in emission of Lean code.
+    #[error(transparent)]
+    Emit(#[from] emit::Error),
+
+    /// Errors in file handling.
+    #[error(transparent)]
+    File(#[from] file::Error),
+}