diff --git a/Cargo.lock b/Cargo.lock index 4c07d18..70542fd 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -161,6 +161,12 @@ dependencies = [ "windows-sys", ] +[[package]] +name = "anyhow" +version = "1.0.87" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "10f00e1f6e58a40e807377c75c6a7f97bf9044fab57816f2414e6f5f4499d7b8" + [[package]] name = "ark-bn254" version = "0.4.0" @@ -512,9 +518,9 @@ dependencies = [ [[package]] name = "clap" -version = "4.5.11" +version = "4.5.17" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "35723e6a11662c2afb578bcf0b88bf6ea8e21282a953428f240574fcc3a2b5b3" +checksum = "3e5a21b8495e732f1b3c364c9949b201ca7bae518c502c80256c96ad79eaf6ac" dependencies = [ "clap_builder", "clap_derive", @@ -522,9 +528,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.5.11" +version = "4.5.17" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "49eb96cbfa7cfa35017b7cd548c75b14c3118c98b423041d70562665e07fb0fa" +checksum = "8cf2dd12af7a047ad9d6da2b6b249759a22a7abc0f474c1dae1777afa4b21a73" dependencies = [ "anstream", "anstyle", @@ -534,9 +540,9 @@ dependencies = [ [[package]] name = "clap_derive" -version = "4.5.11" +version = "4.5.13" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5d029b67f89d30bbb547c89fd5161293c0aec155fc691d7924b64550662db93e" +checksum = "501d359d5f3dcaf6ecdeee48833ae73ec6e42723a1e52419c79abf9507eec0a0" dependencies = [ "heck", "proc-macro2", @@ -1025,6 +1031,12 @@ dependencies = [ "serde", ] +[[package]] +name = "indoc" +version = "2.0.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b248f5224d1d606005e02c97f5aa4e88eeb230488bcc03bc9ca4d7991399f2b5" + [[package]] name = "is_terminal_polyfill" version = "1.70.1" @@ -1055,9 +1067,9 @@ dependencies = [ [[package]] name = "itertools" -version = "0.12.1" +version = "0.13.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ba291022dbbd398a455acf126c1e341954079855bc60dfdda641363bd6922569" +checksum = "413ee7dfc52ee1a4949ceeb7dbc8a33f2d6c088194d9f922fb8318faf1f01186" dependencies = [ "either", ] @@ -1145,10 +1157,18 @@ dependencies = [ name = "lampe" version = "0.1.0" dependencies = [ - "itertools 0.12.1", + "anyhow", + "clap", + "derivative", + "fm", + "indoc", + "itertools 0.13.0", + "log", "nargo", "noirc_driver", + "noirc_errors", "noirc_frontend", + "thiserror", ] [[package]] @@ -1621,9 +1641,9 @@ dependencies = [ [[package]] name = "regex" -version = "1.10.5" +version = "1.10.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b91213439dad192326a0d7c6ee3955910425f441d7038e0d6933b0aec5c4517f" +checksum = "4219d74c6b67a3654a9fbebc4b419e22126d13d2f3c4a07ee0cb61ff79a79619" dependencies = [ "aho-corasick", "memchr", diff --git a/Cargo.toml b/Cargo.toml index b055cad..08cf47f 100644 --- a/Cargo.toml +++ b/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" \ No newline at end of file +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" diff --git a/README.md b/README.md new file mode 100644 index 0000000..92ea09e --- /dev/null +++ b/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. diff --git a/rustfmt.toml b/rustfmt.toml new file mode 100644 index 0000000..8bd3e7d --- /dev/null +++ b/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 diff --git a/src/bin/main.rs b/src/bin/main.rs new file mode 100644 index 0000000..90cb4f3 --- /dev/null +++ b/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 { + 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) +} diff --git a/src/error/compilation.rs b/src/error/compilation.rs new file mode 100644 index 0000000..afb4de8 --- /dev/null +++ b/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 = std::result::Result; + +/// 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 for Error { + fn from(diagnostics: ErrorsAndWarnings) -> Self { + Error::CheckFailure { diagnostics } + } +} diff --git a/src/error/emit.rs b/src/error/emit.rs new file mode 100644 index 0000000..9bcff87 --- /dev/null +++ b/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 = std::result::Result; + +/// 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, +} diff --git a/src/error/file.rs b/src/error/file.rs new file mode 100644 index 0000000..c8c2a1b --- /dev/null +++ b/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 = std::result::Result; + +/// 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), +} diff --git a/src/error/mod.rs b/src/error/mod.rs new file mode 100644 index 0000000..5003c84 --- /dev/null +++ b/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 = std::result::Result; + +/// 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), +} diff --git a/src/lean/indent.rs b/src/lean/indent.rs new file mode 100644 index 0000000..7cb6718 --- /dev/null +++ b/src/lean/indent.rs @@ -0,0 +1,149 @@ +//! A container for Lean source-code expressions. + +use itertools::Itertools; + +use crate::error::emit::{Error, Result}; + +/// The default string used for each indentation level. +const DEFAULT_INDENT_STRING: &str = " "; + +/// The default line separator. +const DEFAULT_LINE_SEPARATOR: &str = "\n"; + +/// A stateful handler for the current level of indentation of strings being +/// built. +#[derive(Clone, Debug, PartialEq, PartialOrd)] +pub struct Indenter { + /// The string replicated for each indentation level. + indent_string: String, + + /// The character(s) used to separate lines. + line_separator: String, + + /// The current indentation level. + current_level: usize, +} +impl Indenter { + /// Creates a new indenter configured to use the `indent_string` and + /// `line_separator` with a default indentation level of zero. + pub fn new(indent_string: impl Into, line_separator: impl Into) -> Self { + let current_level = 0; + let indent_string = indent_string.into(); + let line_separator = line_separator.into(); + Self { + indent_string, + line_separator, + current_level, + } + } + + /// Returns the line separator in use. + #[must_use] + pub fn sep(&self) -> &str { + &self.line_separator + } + + /// Gets the current indentation level. + #[must_use] + pub fn level(&self) -> usize { + self.current_level + } + + /// Increases the current indentation level by one. + pub fn indent(&mut self) { + self.current_level += 1; + } + + /// Decreases the current indentation level by one. + /// + /// # Errors + /// + /// - [`Error::CannotDecreaseIndentLevel`] if the indentation level is + /// already zero and a decrease in that level is requested. + pub fn dedent(&mut self) -> Result<()> { + if self.current_level != 0 { + self.current_level -= 1; + Ok(()) + } else { + Err(Error::CannotDecreaseIndentLevel) + } + } + + /// Performs indenting on the provided input. + pub fn run(&self, input: impl Into) -> String { + let input: String = input.into(); + let indent = self.indent_string.repeat(self.current_level); + + input + .split(self.line_separator.as_str()) + .map(|line| format!("{indent}{line}")) + .join(self.line_separator.as_str()) + } +} + +impl Default for Indenter { + fn default() -> Self { + Self::new(DEFAULT_INDENT_STRING, DEFAULT_LINE_SEPARATOR) + } +} + +#[cfg(test)] +mod test { + use crate::{error::emit::Error, lean::indent::Indenter}; + + #[test] + fn can_modify_indent_level() -> anyhow::Result<()> { + let mut indenter = Indenter::default(); + + assert_eq!(indenter.level(), 0); + indenter.indent(); + assert_eq!(indenter.level(), 1); + indenter.dedent()?; + assert_eq!(indenter.level(), 0); + + Ok(()) + } + + #[test] + fn can_indent_source_text() -> anyhow::Result<()> { + let mut indenter = Indenter::default(); + let text = "foo"; + + assert_eq!(indenter.run(text), text); + indenter.indent(); + assert_eq!(indenter.run(text), format!(" {text}")); + indenter.indent(); + assert_eq!(indenter.run(text), format!(" {text}")); + indenter.dedent()?; + assert_eq!(indenter.run(text), format!(" {text}")); + + Ok(()) + } + + #[test] + fn correctly_indents_multiline_text() { + let mut indenter = Indenter::default(); + let text = "foo\n bar\n baz"; + + indenter.indent(); + assert_eq!(indenter.run(text), " foo\n bar\n baz"); + } + + #[test] + fn can_use_specific_indent_strings() { + let mut indenter = Indenter::new("--", "\n"); + let text = "foo"; + + indenter.indent(); + assert_eq!(indenter.run(text), "--foo"); + } + + #[test] + fn errors_on_decreasing_indent_level_too_far() { + let mut indenter = Indenter::default(); + + let result = indenter.dedent(); + assert!(result.is_err()); + assert_eq!(result.unwrap_err(), Error::CannotDecreaseIndentLevel); + } +} diff --git a/src/lean/mod.rs b/src/lean/mod.rs new file mode 100644 index 0000000..2eb69fc --- /dev/null +++ b/src/lean/mod.rs @@ -0,0 +1,1117 @@ +//! Functionality for emitting Lean definitions from Noir source. +pub mod indent; + +use std::collections::HashSet; + +use fm::FileId; +use indoc::formatdoc; +use itertools::Itertools; +use noirc_frontend::{ + ast::{BinaryOpKind, UnaryOp, Visibility}, + graph::CrateId, + hir::{ + def_map::{ModuleData, ModuleId}, + Context, + }, + hir_def::{ + expr::{HirArrayLiteral, HirIdent}, + function::Parameters, + stmt::{HirLValue, HirPattern}, + traits::TraitImpl, + }, + macros_api::{HirExpression, HirLiteral, HirStatement, ModuleDefId, StructId}, + node_interner::{DefinitionKind, ExprId, FuncId, GlobalId, StmtId, TraitId, TypeAliasId}, + Type, +}; + +use crate::{ + error::emit::{Error, Result}, + lean::indent::Indenter, + noir::project::KnownFiles, +}; + +/// The stringified Lean definitions corresponding to a Noir module. +pub type ModuleEntries = Vec; + +/// An emitter for specialized Lean definitions based on the corresponding Noir +/// intermediate representation. +pub struct LeanEmitter { + /// The compilation context of the Noir project. + pub context: Context<'static, 'static>, + + /// The files that were explicitly added to the compilation context. + /// + /// This will contain the file IDs for files added manually during + /// extraction tool execution, and not identifiers for files in the standard + /// library and other implicit libraries. These are used for filtering to + /// prevent emission of definitions for the standard library that are + /// already carefully manually defined in Lean. + known_files: KnownFiles, + + /// The identifier for the root crate in the Noir compilation context. + root_crate: CrateId, +} + +impl LeanEmitter { + /// Creates a new emitter for Lean source code. + /// + /// The emitter wraps the current noir compilation `context`, and also has + /// knowledge of the `known_files` that were added explicitly to the + /// extraction process by the user. + pub fn new( + context: Context<'static, 'static>, + known_files: KnownFiles, + root_crate: CrateId, + ) -> Self { + Self { + context, + known_files, + root_crate, + } + } + + /// Enables reference tracking in the internal context. + pub fn track_references(&mut self) { + self.context.track_references(); + } + + /// Checks if the emitter knows about the file with the given ID, returning + /// `true` if it does and `false` otherwise. + pub fn knows_file(&self, file: FileId) -> bool { + self.known_files.contains(&file) + } + + /// Gets the identifier of the root crate for this compilation context. + pub fn root_crate(&self) -> CrateId { + self.root_crate + } +} + +impl LeanEmitter { + /// Emits a set of Lean definitions that correspond to the Noir language + /// definitions seen by this emitter. + /// + /// # Errors + /// + /// - [`Error`] if the extraction process fails for any reason. + /// + /// # Panics + /// + /// When encountering a situation that would occur due to a bug in the Noir + /// compiler, or due to programmer error. + pub fn emit(&self) -> Result { + let mut indenter = Indenter::default(); + let mut output = Vec::new(); + + // Emit definitions for each of the modules in the context in an arbitrary + // iteration order + for module in self + .context + .def_map(&self.root_crate()) + .expect("Root crate was missing in compilation context") + .modules() + { + let new_defs = self.emit_module(&mut indenter, module)?; + output.extend(new_defs); + } + + // Remove all entries that are duplicated as we do not necessarily have the + // means to prevent emission of duplicates in all cases + let mut set: HashSet = HashSet::new(); + set.extend(output); + let no_dupes: Vec = set.into_iter().collect(); + + // Smoosh the de-duplicated entries back together to yield a file. + Ok(no_dupes.join("\n")) + } + + /// Emits the Lean source code corresponding to a Noir module based on the + /// `module`'s definition. + /// + /// # Errors + /// + /// - [`Error`] if the extraction process fails for any reason. + pub fn emit_module(&self, ind: &mut Indenter, module: &ModuleData) -> Result { + let mut accumulator = Vec::new(); + + // We start by emitting lines that signal the explicit implementation of a trait + // by a type. + for (_, trait_impl) in self + .context + .def_interner + .trait_implementations + .iter() + .filter(|(_, t)| self.knows_file(t.borrow().file)) + { + accumulator.push(self.emit_trait_impl(&trait_impl.borrow())?); + } + + // We then emit all definitions that correspond to the given module. + for typedef in module.type_definitions().chain(module.value_definitions()) { + let definition = match typedef { + ModuleDefId::FunctionId(id) => self.emit_function_def(ind, id)?, + ModuleDefId::TypeId(id) => self.emit_struct_def(ind, id)?, + ModuleDefId::GlobalId(id) => self.emit_global(ind, id)?, + ModuleDefId::TypeAliasId(id) => self.emit_alias(id)?, + ModuleDefId::TraitId(id) => self.emit_trait(ind, id)?, + ModuleDefId::ModuleId(_) => { + unimplemented!("It is unclear what actually generates these.") + } + }; + + accumulator.push(definition.to_string()); + } + + Ok(accumulator + .into_iter() + .filter(|d| !d.is_empty()) + .map(|d| format!("{d}\n")) + .collect()) + } + + /// Emits the string indicating that a given type has explicitly implemented + /// a given trait. + /// + /// Trait implementations do not appear to carry their method definitions + /// with them, so we instead emit lines that serve as "notices" of a given + /// type implementing a trait. The corresponding method definitions are + /// instead emitted as functions (see [`emit_function`]). + /// + /// # Errors + /// + /// - [`Error`] if the extraction process fails for any reason. + pub fn emit_trait_impl(&self, trait_impl: &TraitImpl) -> Result { + let trait_def_id = trait_impl.trait_id; + let trait_data = self.context.def_interner.get_trait(trait_def_id); + let fq_crate_name = self.fq_trait_name_from_crate_id(trait_data.crate_id, trait_def_id); + let name = &trait_impl.ident; + let full_name = if fq_crate_name.is_empty() { + name.to_string() + } else { + format!("{fq_crate_name}::{name}") + }; + let target = self.emit_fully_qualified_type(&trait_impl.typ); + + let generics = &trait_impl + .trait_generics + .iter() + .map(|g| self.emit_fully_qualified_type(g)) + .collect_vec(); + let trait_gens = generics.join(", "); + + Ok(format!("impl {full_name}<{trait_gens}> for {target};")) + } + + /// Emits Lean code corresponding to a trait definition in Noir. + /// + /// Note that this doesn't currently contend with associated types or consts + /// in traits due to a strange indexing issue that may or may not be a Noir + /// compiler bug. + /// + /// # Errors + /// + /// - [`Error`] if the extraction process fails for any reason. + pub fn emit_trait(&self, ind: &mut Indenter, trait_id: TraitId) -> Result { + let trait_data = self.context.def_interner.get_trait(trait_id); + let trait_name = &trait_data.name; + let fq_crate_name = self.fq_trait_name_from_crate_id(trait_data.crate_id, trait_id); + let full_name = if fq_crate_name.is_empty() { + trait_name.to_string() + } else { + format!("{fq_crate_name}::{trait_name}") + }; + let generics = trait_data.generics.iter().map(|g| g.name.clone()).join(", "); + + let method_strings = &trait_data + .methods + .iter() + .map(|method| { + let name = &method.name; + let generics = method.direct_generics.iter().map(|g| &g.name).join(", "); + let typ = self.emit_fully_qualified_type(&method.typ); + + // We ignore defaults as they appear to be instantiated by this point for + // implementing types. + format!("fn {name}<{generics}> : {typ};") + }) + .collect_vec(); + + ind.indent(); + let methods = ind.run(method_strings.join("\n")); + ind.dedent()?; + + let trait_def = formatdoc! { + r"trait {full_name}<{generics}> {{ + {methods} + }}" + }; + + Ok(trait_def) + } + + /// Emits the Lean code corresponding to a type alias in Noir. + /// + /// # Errors + /// + /// - [`Error`] if the extraction process fails for any reason. + pub fn emit_alias(&self, alias: TypeAliasId) -> Result { + let alias_data = self.context.def_interner.get_type_alias(alias); + let alias_data = alias_data.borrow(); + let alias_name = &alias_data.name; + let generics = alias_data + .generics + .iter() + .map(|g| { + let gen = &g.name; + format!("{gen}") + }) + .join(", "); + let typ = self.emit_fully_qualified_type(&alias_data.typ); + + Ok(format!("type {alias_name}<{generics}> = {typ};")) + } + + /// Emits the Lean code corresponding to a Noir global definition. + /// + /// # Errors + /// + /// - [`Error`] if the extraction process fails for any reason. + pub fn emit_global(&self, ind: &mut Indenter, global: GlobalId) -> Result { + let global_data = self.context.def_interner.get_global(global); + let value = self.emit_statement(ind, global_data.let_statement)?; + + Ok(format!("global {value}")) + } + + /// Emits the Lean source code corresponding to a Noir structure at the + /// module level. + /// + /// # Errors + /// + /// - [`Error`] if the extraction process fails for any reason. + pub fn emit_struct_def(&self, ind: &mut Indenter, s: StructId) -> Result { + let struct_data = self.context.def_interner.get_struct(s); + let struct_data = struct_data.borrow(); + let fq_path = self + .context + .fully_qualified_struct_path(&struct_data.id.module_id().krate, s); + let generics = &struct_data.generics; + let generics_string = generics.iter().map(|g| &g.name).join(", "); + let fields = struct_data.get_fields_as_written(); + + // We generate the fields under a higher indentation level to make it look nice + ind.indent(); + let field_strings = fields + .iter() + .map(|(name, typ)| { + ind.run(format!( + "{name} : {typ}", + typ = self.emit_fully_qualified_type(typ) + )) + }) + .collect_vec(); + ind.dedent()?; + + let fields_string = field_strings.join(",\n"); + + let result = formatdoc! { + r"nr_struct {fq_path}<{generics_string}> {{ + {fields_string} + }}" + }; + + Ok(result) + } + + /// Emits the Lean source code corresponding to a Noir function at the + /// module level. + /// + /// # Errors + /// + /// - [`Error`] if the extraction process fails for any reason. + pub fn emit_function_def(&self, ind: &mut Indenter, func: FuncId) -> Result { + // Get the various parameters + let func_data = self.context.function_meta(&func); + let generics = &func_data.all_generics; + let fq_path = self + .context + .fully_qualified_function_name(&func_data.source_crate, &func); + let generics_string = generics.iter().map(|g| &g.name).join(", "); + let parameters = self.function_param_string(&func_data.parameters)?; + let ret_type = self.emit_fully_qualified_type(func_data.return_type()); + let assoc_trait_string = match func_data.trait_impl { + Some(trait_id) => { + let impl_data = self.context.def_interner.get_trait_implementation(trait_id); + let impl_data = impl_data.borrow(); + let trait_data = self.context.def_interner.get_trait(impl_data.trait_id); + let fq_crate_name = + self.fq_trait_name_from_crate_id(trait_data.crate_id, impl_data.trait_id); + let trait_name = &trait_data.name; + let impl_type = self.emit_fully_qualified_type(&impl_data.typ); + + let impl_generics = &impl_data + .trait_generics + .iter() + .map(|g| self.emit_fully_qualified_type(g)) + .collect_vec(); + let generics_str = impl_generics.join(", "); + + let fq_trait_name = if fq_crate_name.is_empty() { + format!("{trait_name}<{generics_str}>") + } else { + format!("{fq_crate_name}::{trait_name}<{generics_str}>") + }; + + format!("({impl_type} as {fq_trait_name})::") + } + None => String::new(), + }; + + // Generate the function body ready for insertion + ind.indent(); + let body = self.emit_expr(ind, self.context.def_interner.function(&func).as_expr())?; + ind.dedent()?; + + let self_type_str = match &func_data.self_type { + Some(ty) => { + let fq_type = self.emit_fully_qualified_type(ty); + format!("{fq_type}::") + } + _ => String::new(), + }; + + // Now we can actually build our function + let result = formatdoc! { + r"nr_def {assoc_trait_string}{self_type_str}{fq_path}<{generics_string}>({parameters}) -> {ret_type} {{ + {body} + }}" + }; + + if result.contains("nr_def _::") { + // This is a dummy trait method that we don't care about, so we discard it. + Ok(String::new()) + } else { + Ok(result) + } + } + + /// Emits a fully-qualified type name for types where this is relevant. + /// + /// The correct operation of this function relies on type resolution having + /// been conducted properly by the Noir compiler. Absent that, it may return + /// nonsensical results. + /// + /// # Panics + /// + /// When encountering situations that would indicate a bug in the Noir + /// compiler. + pub fn emit_fully_qualified_type(&self, typ: &Type) -> String { + let str: String = match typ { + Type::Array(elem_type, size) => { + let elem_type = self.emit_fully_qualified_type(elem_type); + + format!("[{elem_type}; {size}]") + } + Type::Slice(elem_type) => { + let elem_type = self.emit_fully_qualified_type(elem_type); + + format!("[{elem_type}]") + } + Type::Tuple(elems) => { + let elem_types = elems + .iter() + .map(|typ| self.emit_fully_qualified_type(typ)) + .collect_vec(); + let elems_str = elem_types.join(", "); + + format!("({elems_str})") + } + Type::Struct(struct_type, generics) => { + let struct_type = struct_type.borrow(); + let module_id = struct_type.id.module_id(); + let name = self + .context + .fully_qualified_struct_path(&module_id.krate, struct_type.id); + + let generics_resolved = generics + .iter() + .map(|g| self.emit_fully_qualified_type(g)) + .collect_vec(); + let generics_str = generics_resolved.join(", "); + + format!("{name}<{generics_str}>") + } + Type::TraitAsType(trait_id, name, generics) => { + let module_id = trait_id.0; + let module_path = self.fq_module_name_from_mod_id(module_id); + + let generics_resolved = generics + .iter() + .map(|g| self.emit_fully_qualified_type(g)) + .collect_vec(); + let generics_str = generics_resolved.join(", "); + + if module_path.is_empty() { + format!("{name}<{generics_str}>") + } else { + format!("{module_path}::{name}<{generics_str}>") + } + } + Type::Function(args, ret, environment) => { + let arg_types = args + .iter() + .map(|arg| self.emit_fully_qualified_type(arg)) + .collect_vec(); + let arg_types_str = arg_types.join(", "); + let ret_str = self.emit_fully_qualified_type(ret); + + let env_string = environment.to_string(); + let env_string = env_string + .strip_prefix("(") + .expect("Environment did not contain a tuple type") + .strip_suffix(")") + .expect("Environment did not contain a tuple type"); + format!("{{{env_string}}} -> ({arg_types_str}) -> {ret_str}") + } + Type::MutableReference(typ) => { + let typ_str = self.emit_fully_qualified_type(typ); + format!("&mut {typ_str}") + } + // In all the other cases we can use the default printing as internal type vars are + // non-existent, constrained to be types we don't care about customizing, or are + // non-existent in the phase the emitter runs after. + _ => format!("{typ}"), + }; + + str + } + + /// Generates a fully-qualified module name from a module id. + /// + /// # Panics + /// + /// When encountering a situation that would occur due to a bug in the Noir + /// compiler. + pub fn fq_module_name_from_mod_id(&self, id: ModuleId) -> String { + let krate = self + .context + .def_map(&id.krate) + .expect("Module should exist in context"); + let (ix, data) = krate + .modules() + .iter() + .find(|(i, _)| *i == id.local_id.0) + .expect("Module should exist in context"); + let module_path = krate.get_module_path_with_separator(ix, data.parent, "::"); + + if id.krate.is_stdlib() { + format!("std::{module_path}") + } else { + module_path + } + } + + /// Generates a fully-qualified module name from a crate id. + /// + /// # Panics + /// + /// When encountering a situation that would occur due to a bug in the Noir + /// compiler. + pub fn fq_trait_name_from_crate_id(&self, id: CrateId, trait_id: TraitId) -> String { + let krate = self.context.def_map(&id).expect("Module should exist in context"); + let (ix, data) = krate + .modules() + .iter() + .find(|(_, m)| { + let mut type_defs = m.type_definitions(); + type_defs.any(|item| match item { + ModuleDefId::TraitId(trait_id_inner) => trait_id == trait_id_inner, + _ => false, + }) + }) + .expect("Should work"); + let module_path = krate.get_module_path_with_separator(ix, data.parent, "::"); + + if id.is_stdlib() { + format!("std::{module_path}") + } else { + module_path + } + } + + /// Emits the Lean source code corresponding to a Noir expression. + /// + /// # Errors + /// + /// - [`Error`] if the extraction process fails for any reason. + /// + /// # Panics + /// + /// When encountering macros, which should have been eliminated by the Noir + /// compilation process before calling this function. + #[allow(clippy::too_many_lines)] // Not possible to reasonably split up + pub fn emit_expr(&self, ind: &mut Indenter, expr: ExprId) -> Result { + let expr_data = self.context.def_interner.expression(&expr); + + let expression = match expr_data { + HirExpression::Block(block) => { + let statements: Vec = block + .statements + .iter() + .map(|stmt| { + let stmt_line = self.emit_statement(ind, *stmt)?; + Ok(ind.run(stmt_line)) + }) + .try_collect()?; + statements.join("\n") + } + HirExpression::Infix(infix) => { + let lhs = self.emit_expr(ind, infix.lhs)?; + let rhs = self.emit_expr(ind, infix.rhs)?; + let op_name = self.emit_binary_operator(infix.operator.kind); + + format!("{op_name}({lhs}, {rhs})") + } + HirExpression::Ident(ident, _generics) => { + let name = self.context.def_interner.definition_name(ident.id); + let ident_def = self.context.def_interner.definition(ident.id); + + match ident_def.kind { + DefinitionKind::Function(func) => { + let id_type = self.context.def_interner.id_type(expr); + let function_info = self.context.def_interner.function_meta(&func); + let func_sig = self.emit_fully_qualified_type(&id_type); + let generics = function_info + .all_generics + .iter() + .map(|g| { + let name = &g.name; + let kind = &g.kind; + + format!("{name} <: {kind}") + }) + .join(", "); + let fn_type = format!("<{generics}> => {func_sig}"); + let self_type = match &function_info.self_type.as_ref() { + Some(s) => self.emit_fully_qualified_type(s), + None => String::new(), + }; + + let fn_name = if self_type.is_empty() { + name.to_string() + } else { + format!("{self_type}::{name}") + }; + + format!("({fn_name} : {fn_type})") + } + DefinitionKind::Global(global) => { + let global_info = self.context.def_interner.get_global(global); + let ident_type = self.context.def_interner.definition_type(ident.id); + let resolved_type = self.emit_fully_qualified_type(&ident_type); + let value = global_info + .value + .as_ref() + .map(|v| format!(" = {v}")) + .unwrap_or_default(); + + format!("({name} : {resolved_type}{value})") + } + _ => { + let ident_type = self.context.def_interner.definition_type(ident.id); + let resolved_type = self.emit_fully_qualified_type(&ident_type); + + format!("({name} : {resolved_type})") + } + } + } + HirExpression::Index(index) => { + let collection = self.emit_expr(ind, index.collection)?; + let index = self.emit_expr(ind, index.index)?; + + format!("{collection}[{index}]") + } + HirExpression::Literal(lit) => self.emit_literal(ind, lit, expr)?, + HirExpression::Prefix(prefix) => { + let rhs = self.emit_expr(ind, prefix.rhs)?; + let op = self.emit_unary_operator(prefix.operator); + + format!("{op}({rhs})") + } + HirExpression::Constructor(constructor) => { + let struct_def = constructor.r#type; + let struct_def = struct_def.borrow(); + let name = &struct_def.name; + let fields = constructor.fields; + let generics = constructor.struct_generics; + + let generics_strings = generics + .iter() + .map(|generic| self.emit_fully_qualified_type(generic)) + .collect_vec(); + let generics_string = generics_strings.join(", "); + + let fields_strings: Vec = fields + .iter() + .map(|(name, expr)| { + let expr_str = self.emit_expr(ind, *expr)?; + Ok(format!("{name}: {expr_str}")) + }) + .try_collect()?; + let fields_string = ind.run(fields_strings.join(",\n")); + + let result = formatdoc! { + r"{name}.mk <{generics_string}> {{ + {fields_string} + }}" + }; + + result + } + HirExpression::MemberAccess(member) => { + let target = self.emit_expr(ind, member.lhs)?; + let member = member.rhs; + + format!("{target}.{member}") + } + HirExpression::Call(call) => { + assert!( + !call.is_macro_call, + "Macros should be resolved before running this tool" + ); + + let function = self.emit_expr(ind, call.func)?; + + let out_args: Vec = call + .arguments + .iter() + .map(|arg| self.emit_expr(ind, *arg)) + .try_collect()?; + let args_string = out_args.join(", "); + + format!("{function}({args_string})") + } + HirExpression::MethodCall(method_call) => { + let receiver = self.emit_expr(ind, method_call.object)?; + let generics = match method_call.generics { + Some(gs) => { + let generic_strings = + gs.iter().map(|g| self.emit_fully_qualified_type(g)).collect_vec(); + generic_strings.join(", ") + } + _ => String::new(), + }; + + let arguments: Vec = method_call + .arguments + .iter() + .map(|arg| self.emit_expr(ind, *arg)) + .try_collect()?; + let args_string = arguments.join(", "); + + format!("{receiver}<{generics}>({args_string})") + } + HirExpression::Cast(cast) => { + let source = self.emit_expr(ind, cast.lhs)?; + let target_type = self.emit_fully_qualified_type(&cast.r#type); + + format!("{source} as {target_type}") + } + HirExpression::If(if_expr) => { + let if_cond = self.emit_expr(ind, if_expr.condition)?; + let then_exec = self.emit_expr(ind, if_expr.consequence)?; + + match if_expr.alternative { + Some(else_exec) => { + let else_exec = self.emit_expr(ind, else_exec)?; + + formatdoc! { + r"if {if_cond} {{ + {then_exec} + }} else {{ + {else_exec} + }}" + } + } + None => { + formatdoc! { + r"if {if_cond} {{ + {then_exec} + }}" + } + } + } + } + HirExpression::Tuple(tuple) => { + let item_exprs: Vec = + tuple.iter().map(|expr| self.emit_expr(ind, *expr)).try_collect()?; + let items = item_exprs.join(", "); + + format!("({items})") + } + HirExpression::Lambda(lambda) => { + let ret_type = self.emit_fully_qualified_type(&lambda.return_type); + + let arg_strs: Vec = lambda + .parameters + .iter() + .map(|(pattern, ty)| { + let pattern_str = self.emit_pattern(pattern)?; + let typ = self.emit_fully_qualified_type(ty); + + Ok(format!("{pattern_str} : {typ}")) + }) + .try_collect()?; + let args = arg_strs.join(", "); + + let captures = lambda + .captures + .iter() + .map(|capture| { + let capture_type = + self.context.def_interner.definition_type(capture.ident.id); + let name = self.context.def_interner.definition_name(capture.ident.id); + + format!("{name} : {capture_type}") + }) + .join(", "); + + let body = self.emit_expr(ind, lambda.body)?; + + format!("(| {{{captures}}}, ({args}) | {body}): {ret_type}") + } + HirExpression::Comptime(_) => { + panic!("Comptime expressions should not exist after compilation is done") + } + HirExpression::Quote(_) => { + panic!("Quote expressions should not exist after macro resolution") + } + HirExpression::Unquote(_) => { + panic!("Unquote expressions should not exist after macro resolution") + } + HirExpression::Error => panic!("Encountered error expression where none should exist"), + }; + + Ok(expression) + } + + /// Emits the Lean source code corresponding to a Noir statement. + /// + /// # Errors + /// + /// - [`Error`] if the extraction process fails for any reason. + /// + /// # Panics + /// + /// Upon reaching an unsupported construct that should have been eliminated + /// by the Noir compiler at the point this function is called. + pub fn emit_statement(&self, ind: &mut Indenter, statement: StmtId) -> Result { + let stmt_data = self.context.def_interner.statement(&statement); + + let result = match stmt_data { + HirStatement::Expression(expr) => self.emit_expr(ind, expr)?, + HirStatement::Let(lets) => { + let binding_type = self.emit_fully_qualified_type(&lets.r#type); + let bound_expr = self.emit_expr(ind, lets.expression)?; + let name = self.emit_pattern(&lets.pattern)?; + + format!("let {name}: {binding_type} = {bound_expr}") + } + HirStatement::Constrain(constraint) => { + let constraint_expr = self.emit_expr(ind, constraint.0)?; + + if let Some(expr) = constraint.2 { + let print_expr = self.emit_expr(ind, expr)?; + format!("assert({constraint_expr}, {print_expr})") + } else { + format!("assert({constraint_expr})") + } + } + HirStatement::Assign(assign) => { + let l_val = self.emit_l_value(ind, &assign.lvalue)?; + let expr = self.emit_expr(ind, assign.expression)?; + + format!("{l_val} = {expr}") + } + HirStatement::For(fors) => { + let loop_var = self.context.def_interner.definition_name(fors.identifier.id); + let loop_start = self.emit_expr(ind, fors.start_range)?; + let loop_end = self.emit_expr(ind, fors.end_range)?; + let body = self.emit_expr(ind, fors.block)?; + + formatdoc! { + r"for {loop_var} in {loop_start} .. {loop_end} {{ + {body} + }} + " + } + } + HirStatement::Break => "break".into(), + HirStatement::Continue => "continue".into(), + HirStatement::Semi(semi) => self.emit_expr(ind, semi)?, + HirStatement::Comptime(_) => { + panic!("Comptime statements should not exist after compilation") + } + HirStatement::Error => panic!("Encountered error statement where none should exist"), + }; + + Ok(format!("{result};")) + } + + /// Generates a Lean representation of a Noir l-value (something that can be + /// assigned to). + /// + /// # Errors + /// + /// - [`Error`] if the extraction process fails for any reason. + pub fn emit_l_value(&self, ind: &mut Indenter, l_val: &HirLValue) -> Result { + let result = match l_val { + HirLValue::Ident(ident, ty) => { + let ident_str = self.context.def_interner.definition_name(ident.id); + let ty_str = self.emit_fully_qualified_type(ty); + format!("({ident_str} : {ty_str})") + } + HirLValue::MemberAccess { + object, + field_name, + typ, + .. + } => { + let obj_str = self.emit_l_value(ind, object.as_ref())?; + let typ_str = self.emit_fully_qualified_type(typ); + + format!("({obj_str}.{field_name} : {typ_str})") + } + HirLValue::Index { + array, index, typ, .. + } => { + let array_expr = self.emit_l_value(ind, array.as_ref())?; + let ix_expr = self.emit_expr(ind, *index)?; + let typ_str = self.emit_fully_qualified_type(typ); + + format!("({array_expr}[{ix_expr}] : {typ_str})") + } + HirLValue::Dereference { + lvalue, + element_type, + .. + } => { + let l_val_expr = self.emit_l_value(ind, lvalue.as_ref())?; + let elem_ty = self.emit_fully_qualified_type(element_type); + + format!("(*{l_val_expr} : {elem_ty})") + } + }; + + Ok(result) + } + + /// Emits the Lean code corresponding to a Noir pattern. + /// + /// # Errors + /// + /// - [`Error`] if the extraction process fails for any reason. + pub fn emit_pattern(&self, pattern: &HirPattern) -> Result { + let result = match pattern { + HirPattern::Identifier(id) => { + self.context.def_interner.definition_name(id.id).to_string() + } + HirPattern::Mutable(pattern, _) => { + let child_pattern = self.emit_pattern(pattern.as_ref())?; + format!("mut {child_pattern}") + } + HirPattern::Tuple(patterns, _) => { + let pattern_strs: Vec = patterns + .iter() + .map(|pattern| self.emit_pattern(pattern)) + .try_collect()?; + let patterns_str = pattern_strs.join(", "); + + format!("({patterns_str})") + } + HirPattern::Struct(struct_ty, patterns, _) => { + let ty_str = self.emit_fully_qualified_type(struct_ty); + + let pattern_strs: Vec = patterns + .iter() + .map(|(pat_name, pat_expr)| { + let child_pat = self.emit_pattern(pat_expr)?; + + Ok(format!("{pat_name}: {child_pat}")) + }) + .try_collect()?; + let patterns_str = pattern_strs.join(", "); + + format!("{ty_str} {{{patterns_str}}}") + } + }; + + Ok(result) + } + + /// Emits the Lean source code corresponding to a Noir literal. + /// + /// # Errors + /// + /// - [`Error`] if the extraction process fails for any reason. + pub fn emit_literal( + &self, + ind: &mut Indenter, + literal: HirLiteral, + expr: ExprId, + ) -> Result { + let result = match literal { + HirLiteral::Array(array) => self.emit_array_literal(ind, array)?, + HirLiteral::Slice(slice) => { + let array_lit = self.emit_array_literal(ind, slice)?; + format!("&{array_lit}") + } + HirLiteral::Bool(bool) => { + if bool { + "true".to_string() + } else { + "false".to_string() + } + } + HirLiteral::Integer(felt, neg) => { + let typ = self.context.def_interner.id_type(expr).to_string(); + format!("{minus}{felt} : {typ}", minus = if neg { "-" } else { "" }) + } + HirLiteral::Str(str) => { + format!(r#""{str}""#) + } + HirLiteral::FmtStr(template, exprs) => { + let expr_strings: Vec = + exprs.iter().map(|expr| self.emit_expr(ind, *expr)).try_collect()?; + let exprs = expr_strings.join(", "); + + format!(r#""{template}".fmt({exprs})"#) + } + HirLiteral::Unit => "()".into(), + }; + + Ok(result) + } + + /// Emits the Lean code corresponding to a Noir array literal. + /// + /// # Errors + /// + /// - [`Error`] if the extraction process fails for any reason. + pub fn emit_array_literal( + &self, + ind: &mut Indenter, + literal: HirArrayLiteral, + ) -> Result { + let result = match literal { + HirArrayLiteral::Standard(elems) => { + let elem_strings: Vec = + elems.iter().map(|elem| self.emit_expr(ind, *elem)).try_collect()?; + let elems_string = elem_strings.join(", "); + + format!("[{elems_string}]") + } + HirArrayLiteral::Repeated { + repeated_element, + length, + } => { + let elem = self.emit_expr(ind, repeated_element)?; + let len_ty = self.emit_fully_qualified_type(&length); + format!("[{elem}; {len_ty}]") + } + }; + + Ok(result) + } + + /// Generates a function parameter string from the provided parameters. + /// + /// # Errors + /// + /// - [`Error`] if the extraction process fails for any reason. + pub fn function_param_string(&self, params: &Parameters) -> Result { + let result_params: Vec = params + .iter() + .map(|(pattern, typ, vis)| { + let name = self + .context + .def_interner + .definition_name(expect_identifier(pattern)?.id); + let vis_string: String = match vis { + Visibility::Public => "pub ", + Visibility::Private => "", + Visibility::CallData(_) => "call_data ", + Visibility::ReturnData => "ret_data ", + } + .into(); + + let qualified_type = self.emit_fully_qualified_type(typ); + + Ok(format!("{name} : {vis_string}{qualified_type}")) + }) + .try_collect()?; + + Ok(result_params.join(", ")) + } + + /// Emits the Lean source code corresponding to a Noir binary operator. + pub fn emit_binary_operator(&self, op: BinaryOpKind) -> String { + match op { + BinaryOpKind::Add => "nr_add", + BinaryOpKind::And => "nr_and", + BinaryOpKind::Divide => "nr_div", + BinaryOpKind::Equal => "nr_eq", + BinaryOpKind::Greater => "nr_gt", + BinaryOpKind::GreaterEqual => "nr_geq", + BinaryOpKind::Less => "nr_lt", + BinaryOpKind::LessEqual => "nr_leq", + BinaryOpKind::Modulo => "nr_mod", + BinaryOpKind::Multiply => "nr_mul", + BinaryOpKind::NotEqual => "nr_neq", + BinaryOpKind::Or => "nr_or", + BinaryOpKind::ShiftLeft => "nr_shl", + BinaryOpKind::ShiftRight => "nr_shr", + BinaryOpKind::Subtract => "nr_sub", + BinaryOpKind::Xor => "nr_xor", + } + .into() + } + + /// Emits the Lean source code corresponding to a Noir unary operator. + pub fn emit_unary_operator(&self, op: UnaryOp) -> String { + match op { + UnaryOp::Not => "nr_not", + UnaryOp::Minus => "nr_uminus", + UnaryOp::MutableReference => "nr_ref_mut", + UnaryOp::Dereference { implicitly_added } => { + if implicitly_added { + "nr_deref_implicit" + } else { + "nr_deref_explicit" + } + } + } + .into() + } +} + +/// Expects that the provided pattern is an HIR identifier. +/// +/// # Errors +/// +/// - [`Error::MissingIdentifier`] if the provided `pattern` is not an +/// identifier. +pub fn expect_identifier(pattern: &HirPattern) -> Result<&HirIdent> { + match pattern { + HirPattern::Identifier(ident) => Ok(ident), + _ => Err(Error::MissingIdentifier(format!("{pattern:?}"))), + } +} + +impl From for Context<'static, 'static> { + fn from(value: LeanEmitter) -> Self { + value.context + } +} + +// TODO Proper emit tests diff --git a/src/lib.rs b/src/lib.rs new file mode 100644 index 0000000..5759fec --- /dev/null +++ b/src/lib.rs @@ -0,0 +1,190 @@ +//! A library for extracting [Noir](https://noir-lang.org) programs to +//! equivalent definitions in the [Lean](https://lean-lang.org) theorem prover +//! and programming language. +//! +//! It provides functionality for ingesting a Noir project, compiling it from +//! source, and then generating definitions in a Lean DSL that provides the +//! proof assistant with all the information necessary to formally verify the +//! program. + +#![warn(clippy::all, clippy::cargo, clippy::pedantic)] +// Allows for better API naming +#![allow(clippy::module_name_repetitions)] +// These occur in our Noir dependencies and cannot be avoided. +#![allow(clippy::multiple_crate_versions)] + +pub mod error; +pub mod lean; +pub mod noir; + +/// The result type for use with the library, exported here for easy access. +pub use crate::error::Result; +/// The project type for use with the library, exported here for easy access. +pub use crate::noir::project::Project; +/// The source type for use with the library, exported here for easy access. +pub use crate::noir::source::Source; + + +/// Takes the definition of a Noir project and converts it into equivalent +/// definitions in the Lean theorem prover and programming language. +/// +/// # Errors +/// +/// If the extraction process fails for any reason. +pub fn noir_to_lean(project: Project) -> Result> { + let lean_emitter = project.compile()?; + let source = lean_emitter.emit()?; + Ok(noir::WithWarnings::new(source, lean_emitter.warnings)) +} + +#[cfg(test)] +mod test { + use std::path::Path; + + use crate::{ + noir::{project::Project, source::Source}, + noir_to_lean, + }; + + /// This test is a bit of a mess and exists purely for experimentation. + #[test] + fn runs() -> anyhow::Result<()> { + // Set up our source code + let file_name = Path::new("main.nr"); + let source = r#" + use std::hash::{Hash, Hasher}; + use std::cmp::{Ordering, Ord, Eq}; + use std::default::Default; + + // fn my_func3(a: u8) -> u8 { + // my_func(a) + // } + + // fn my_func(a: u8) -> u8 { + // a + 1 + // } + + // fn my_func2(arr: [u8; 8], b: u8) -> u8 { + // arr[b] + // } + + // fn get_unchecked(a: Option2) -> T { + // a._value + // } + + // fn cast_test(a: u8) -> u64 { + // if a == 0 { + // 0 + // } else { + // a as u64 + // } + // } + + // fn tuple_test(a: u8) -> (u8, u8) { + // let b = | c | c + a + 10; + // (a, a) + // } + + // fn literal_test() -> () { + // let a = 1; + // let b = true; + // let c = false; + // let d = [1; 5]; + // let e = [1, 2, 3]; + // let f = &[]; + // let g = "asdf"; + // let h = f"${g}"; + // } + + // fn assigns(x: u8) { + // let mut y = 3; + // y += x; + // + // let mut foo = Option2::none(); + // foo._is_some = false; + // + // let mut arr = [1, 2]; + // arr[0] = 10; + // } + + // unconstrained fn loop(x: u8) { + // for i in 0 .. x { + // if i == 2 { + // continue; + // } + // + // if i == 5 { + // break; + // } + // } + // } + + // fn check(x: u8) { + // assert(x == 5); + // } + + // global TEST = 1 + 7 + 3; + // + // fn use_global() -> Field { + // TEST + // } + + struct Option2 { + _is_some: bool, + _value: T, + } + + impl Default for Option2 { + fn default() -> Self { + Option2::none() + } + } + + impl Option2 { + /// Constructs a None value + pub fn none() -> Self { + Self { _is_some: false, _value: std::unsafe::zeroed() } + } + + // /// Constructs a Some wrapper around the given value + // pub fn some(_value: T) -> Self { + // Self { _is_some: true, _value } + // } + // + /// True if this Option is None + pub fn is_none(self) -> bool { + !self.is_some() + } + + /// True if this Option is Some + pub fn is_some(self) -> bool { + self._is_some + } + } + + trait MyTrait { + fn foo(self) -> Self { + self + } + } + + impl MyTrait for Option2 { + fn foo(self) -> Self { + self + } + } + "#; + + let source = Source::new(file_name, source); + + // Create our project + let project = Project::new(Path::new(""), source); + + // Execute the compilation step on our project. + let source = noir_to_lean(project)?.take(); + + println!("{source}"); + + Ok(()) + } +} diff --git a/src/main.rs b/src/main.rs deleted file mode 100644 index 3e3f05c..0000000 --- a/src/main.rs +++ /dev/null @@ -1,306 +0,0 @@ -use std::any::Any; -use std::path::Path; -use nargo::parse_all; -use noirc_driver::{file_manager_with_stdlib, prepare_crate}; -use noirc_frontend::{graph::{CrateId, CrateName}, hir::{def_map::parse_file, Context, ParsedFiles}, Type, TypeVariable, TypeVariableId, TypeVariableKind}; -use noirc_frontend::ast::{BinaryOpKind, UnaryOp}; -use noirc_frontend::hir_def::expr::HirIdent; -use noirc_frontend::hir_def::stmt::{HirAssignStatement, HirConstrainStatement, HirForStatement, HirLetStatement, HirLValue, HirPattern}; -use noirc_frontend::macros_api::{HirExpression, HirLiteral, HirStatement, ModuleDefId}; -use noirc_frontend::node_interner::{DefinitionKind, ExprId, FuncId, StmtId}; -use itertools::Itertools; -use noirc_frontend::hir_def::function::FuncMeta; - -fn expect_identifier(pattern: &HirPattern) -> HirIdent { - match pattern { - HirPattern::Identifier(ident) => ident.clone(), - _ => panic!("can only fetch hir ident from HirPattern::Identifier"), - } -} - -fn op_to_lean(op: BinaryOpKind) -> String { - match op { - BinaryOpKind::Equal => "==".to_string(), - BinaryOpKind::NotEqual => "!=".to_string(), - BinaryOpKind::Add => "+".to_string(), - BinaryOpKind::Subtract => "-".to_string(), - BinaryOpKind::Divide => "/".to_string(), - BinaryOpKind::Less => "<".to_string(), - - _ => panic!("unsupported {:?}", op) - } -} - -fn expr_to_lean(context: &Context, exprId: &ExprId, indent: &str) -> String { - let expr = context.def_interner.expression(exprId); - match expr { - HirExpression::Infix(infix) => { - let lhs = expr_to_lean(context, &infix.lhs, indent); - let rhs = expr_to_lean(context, &infix.rhs, indent); - let op = op_to_lean(infix.operator.kind); - format!("({} {} {})", lhs, op, rhs) - } - HirExpression::Prefix(prefix) => { - let rhs = expr_to_lean(context, &prefix.rhs, indent); - let op = match prefix.operator { - UnaryOp::Not => "!", - _ => panic!("unsupported {:?}", prefix.operator) - }; - format!("({}{})", op, rhs) - } - HirExpression::Ident(ident, generics) => { - let def = context.def_interner.definition(ident.id); - let generics2 = context.def_interner.get_instantiation_bindings(*exprId); - println!("assigned gens: {:?}", generics2); - let pfx = match def.kind { - DefinitionKind::Function(id) => { - let fun = context.def_interner.function(&id); - let idType = context.def_interner.id_type(exprId); - match idType { - Type::Function(args, ret, boop) => { - println!("{} -> {}", args.iter().map(|t| format!("{}", t)).join(", "), ret); - let ret = ret.clone(); - println!("{} -> {}", args.iter().map(|t| format!("{}", t)).join(", "), ret); - } - _ => panic!("expected function type, got {:?}", idType) - } - // let id_type_str = format!("{}", idType); - let meta = context.def_interner.function_meta(&id); - println!("all generics: {:?}", meta.all_generics); - let module_id = context.def_interner.function_module(id); - let krate = context.def_map(&module_id.krate).unwrap(); - let name = context.fully_qualified_function_name(&module_id.krate, &id); - let (ix, data) = krate.modules().iter().find(|(i, _)| *i == module_id.local_id.0).unwrap(); - let module = krate.get_module_path_with_separator(ix, data.parent, "::"); - let self_type = match &meta.self_type { - Some(selfType) => format!("{}::", selfType), - None => "".to_string() - }; - module + "::" + self_type.as_str() - } - _ => "".to_string() - }; - let name = pfx + context.def_interner.definition_name(ident.id); - name - } - HirExpression::Call(call) => { - if call.is_macro_call { - panic!("macros should be resolved by now"); - } - - - let func = expr_to_lean(context, &call.func, indent); - let args = call.arguments.iter().map(|arg| expr_to_lean(context, arg, indent)).join(", "); - format!("{}({})", func, args) - } - HirExpression::Cast(cast) => { - format!("({} #as {})", expr_to_lean(context, &cast.lhs, indent), cast.r#type) - } - HirExpression::Literal(HirLiteral::Integer(felt, neg)) => { - if neg { - todo!("negative literals") - } - format!("({}:{})", felt.to_string(), context.def_interner.id_type(exprId).to_string()) - } - HirExpression::Literal(HirLiteral::Bool(b)) => { - if b { - "true".to_string() - } else { - "false".to_string() - } - } - HirExpression::Block(block) => { - let stmts = block.statements.iter().map(|stmt| stmt_to_lean(context, stmt, &format!(" {}", indent))).join("\n"); - format!("{{\n{}\n{}}}", stmts, indent) - } - HirExpression::If(ite) => { - let cond = expr_to_lean(context, &ite.condition, indent); - let then = expr_to_lean(context, &ite.consequence, indent); - let else_ = ite.alternative.map(|e| format!(" else {}", expr_to_lean(context, &e, indent))).unwrap_or("".to_string()); - format!("if {} then {}{}", cond, then, else_) - } - HirExpression::Index(index) => { - let collection = expr_to_lean(context, &index.collection, indent); - let idx = expr_to_lean(context, &index.index, indent); - format!("{}[{}]", collection, idx) - } - HirExpression::Constructor(cons) => { - let cons_name = cons.r#type.borrow().name.clone(); - let ty_args = cons.struct_generics.iter().map(|t| format!("{}", t)).join(", "); - let fields = cons.fields.iter().map(|(name, expr)| { - let expr_str = expr_to_lean(context, expr, indent); - format!("(\"{}\", {})", name, expr_str) - }).join(", "); - format!("Expr.constructor ({}.apply [{}]) [{}]", cons_name, ty_args, fields) - } - - _ => { panic!("nope! {:?}", expr) } - } -} - -fn stmt_to_lean(context: &Context, stmt: &StmtId, indent: &str) -> String { - let stmt = context.def_interner.statement(stmt); - let unindented = match stmt { - HirStatement::Constrain(HirConstrainStatement(expr, _, _)) => { - let expr_str = expr_to_lean(context, &expr, indent); - format!("assert({});", expr_str) - } - HirStatement::Let(HirLetStatement { pattern: HirPattern::Identifier(id), expression, .. }) => { - let name = context.def_interner.definition_name(id.id); - let expr_str = expr_to_lean(context, &expression, indent); - format!("let {} = {};", name, expr_str) - } - HirStatement::Let(HirLetStatement { pattern: HirPattern::Mutable(id, _), expression, .. }) => { - let name = context.def_interner.definition_name(expect_identifier(&id).id); - let expr_str = expr_to_lean(context, &expression, indent); - format!("let mut {} = {};", name, expr_str) - } - HirStatement::Expression(expr) => format!("{};", expr_to_lean(context, &expr, indent)), - HirStatement::For(HirForStatement { start_range, end_range, identifier, block }) => { - let start = expr_to_lean(context, &start_range, indent); - let end = expr_to_lean(context, &end_range, indent); - let name = context.def_interner.definition_name(identifier.id); - let block_str = expr_to_lean(context, &block, indent); - format!("for {} in {}..{} {};", name, start, end, block_str) - } - HirStatement::Assign(HirAssignStatement{lvalue: HirLValue::Ident(id, _), expression}) => { - let name = context.def_interner.definition_name(id.id); - let expr_str = expr_to_lean(context, &expression, indent); - format!("{} = {};", name, expr_str) - }, - _ => panic!("unsupported {:?}", stmt) - }; - format!("{}{}", indent, unindented) -} - -fn func_header(context: &Context, funId: &FuncMeta) -> String { - let fname = context.def_interner.definition_name(funId.name.id); - let params = funId.parameters.iter().map(|(pat, _, _)| { - let name = context.def_interner.definition_name(expect_identifier(pat).id); - name - }).join(", "); - format!("fn {}({})", fname, params) -} - -fn function_to_lean(context: &Context, funId: &FuncId) -> String { - let meta = context.function_meta(funId); - let header = func_header(context, meta); - - let fun = context.def_interner.function(funId); - - let body_str = expr_to_lean(context, &fun.as_expr(), ""); - format!("{} {}", header, body_str) -} - -fn main() { - let root = Path::new(""); - let file_name = Path::new("main.nr"); - let mut file_manager = file_manager_with_stdlib(root); - let source = r" - use std::hash::{Hash, Hasher}; - use std::cmp::{Ordering, Ord, Eq}; - use std::default::Default; - - struct Option2 { - _is_some: bool, - _value: T, - } - - impl Option2 { - /// Constructs a None value - pub fn none() -> Self { - Self { _is_some: false, _value: std::unsafe::zeroed() } - } - - /// Constructs a Some wrapper around the given value - pub fn some(_value: T) -> Self { - Self { _is_some: true, _value } - } - // - // /// True if this Option is None - // pub fn is_none(self) -> bool { - // !self._is_some - // } - // - // /// True if this Option is Some - // pub fn is_some(self) -> bool { - // self._is_some - // } - } - "; - let fid = file_manager.add_file_with_source(file_name, source.to_string()).expect( - "Adding source buffer to file manager should never fail when file manager is empty", - ); - let parsed_files = parse_all(&file_manager); - let mut context = Context::new(file_manager, parsed_files); - context.track_references(); - - - let root_crate_id = prepare_crate(&mut context, file_name); - let check_result = noirc_driver::check_crate(&mut context, root_crate_id, false, false, None); - println!("{:?}", check_result); - // for (trait_id, trait_impl) in context.def_interner.trait_implementations.iter().filter(|(_, imp)| imp.borrow().file == fid) { - // let imp = trait_impl.borrow(); - // println!("impl! id:{:?} of {:?} for {:?}", trait_id, imp.trait_id, imp.typ); - // } - for module in context.def_map(&root_crate_id).unwrap().modules() { - println!("module: {:?}", module.location); - // println!("{:?}", module.parent); - // for def in module.type_definitions() { - // match def { - // ModuleDefId::TraitId(traitId) => { - // let meta = context.def_interner.get_trait(traitId); - // // let tname = context.def_interner.definition_name(traitId); - // println!("trait {} : {:?}", meta.name, meta); - // } - // _ => {} - // } - // } - for def in module.type_definitions() { - match def { - ModuleDefId::TypeId(structId) => { - let meta = context.def_interner.get_struct(structId); - let meta = meta.borrow(); - let name = meta.name.clone(); - // let generics_count = meta.generics.len(); - // let generics: Vec<_> = meta.generics.iter().enumerate().map(|(i, g)| { - // let var_id = TypeVariableId(generics_count - i - 1); - // Type::TypeVariable(TypeVariable::unbound(var_id), TypeVariableKind::Normal) - // }).collect(); - // let fields = meta.get_fields(&generics).iter().map(|(name, tpe)| { - // let tpe_rep = match tpe { - // Type::TypeVariable(tyVar, _) => format!("(BVar {})", tyVar.id().0), - // other => format!("{}", other) - // }; - // format!("(\"{}\", {})", name, tpe_rep) - // }).join(", "); - - // let tname = context.def_interner.definition_name(traitId); - println!("def {} : Lampe.Type", name); - } - other => { - println!("{:?}", other); - } - } - } - for def in module.value_definitions() { - match def { - ModuleDefId::FunctionId(fun) => { - let local_generics = context.function_meta(&fun).all_generics.clone(); - println!("defining gens: {:?}", local_generics); - let tp = context.function_meta(&fun).typ.clone(); - match &tp { - Type::Forall(tvas, tp) => - println!("{:?} -> {}", tvas, tp), - _ => {} - } - println!("{}", tp); - println!("{}", function_to_lean(&context, &fun)); - } - other => { - println!("{:?}", other); - } - } - } - } -} diff --git a/src/noir/mod.rs b/src/noir/mod.rs new file mode 100644 index 0000000..ade2e6f --- /dev/null +++ b/src/noir/mod.rs @@ -0,0 +1,83 @@ +//! This module contains functionality for interacting with the Noir compiler +//! driver, and easing usage of some of its functionality. +//! +//! They are primarily wrappers to make interaction type-safe in ways that this +//! library cares about. + +use std::{ + fmt::Debug, + ops::{Deref, DerefMut}, +}; + +use derivative::Derivative; +use noirc_driver::Warnings; + +pub mod project; +pub mod source; + +/// A container for attaching non-fatal compilation warnings to arbitrary data. +/// +/// It implements [`Deref`] and [`DerefMut`] to allow the warning information to +/// be attached at any point without having to worry about manually extracting +/// the underlying data to access its properties or call it. +/// +/// The warnings can be removed at any time to result in the underlying data. +#[derive(Derivative)] +#[derivative( + Clone(bound = "T: Clone"), + Debug(bound = "T: Debug"), + Default(bound = "T: Default") +)] +pub struct WithWarnings { + /// The data itself. + pub data: T, + + /// Any warnings attached to the data (possibly empty). + pub warnings: Warnings, +} + +impl WithWarnings { + /// Creates a new container to wrap the provided `data` with the provided + /// `warnings`. + pub fn new(data: T, warnings: Warnings) -> Self { + Self { data, warnings } + } + + /// Wraps the provided data into the container without attaching any + /// warnings. + pub fn wrap(data: T) -> Self { + let warnings = Warnings::new(); + Self::new(data, warnings) + } + + /// Drops any warnings associated with the data to yield only the data. + pub fn take(self) -> T { + self.data + } + + /// Returns `true` if `self` has warnings associated with it, and `false` + /// otherwise. + pub fn has_warnings(&self) -> bool { + !self.warnings.is_empty() + } +} + +impl From for WithWarnings { + fn from(value: T) -> Self { + Self::wrap(value) + } +} + +impl Deref for WithWarnings { + type Target = T; + + fn deref(&self) -> &Self::Target { + &self.data + } +} + +impl DerefMut for WithWarnings { + fn deref_mut(&mut self) -> &mut Self::Target { + &mut self.data + } +} diff --git a/src/noir/project.rs b/src/noir/project.rs new file mode 100644 index 0000000..362a26b --- /dev/null +++ b/src/noir/project.rs @@ -0,0 +1,141 @@ +//! Functionality for working with projects of Noir sources. + +use std::{ + collections::HashSet, + path::{Path, PathBuf}, +}; + +use fm::{FileId, FileManager}; +use nargo::parse_all; +use noirc_driver::{check_crate, file_manager_with_stdlib, prepare_crate}; +use noirc_frontend::hir::Context; + +use crate::{ + error::{ + compilation::{Error as CompileError, Result as CompileResult}, + file::{Error as FileError, Result as FileResult}, + }, + lean::LeanEmitter, + noir::{source::Source, WithWarnings}, +}; + +/// A type for file identifiers that are known to the extraction process. +pub type KnownFiles = HashSet; + +/// A manager for source files for the Noir project that we intend to extract. +#[derive(Clone, Debug)] +pub struct Project { + /// The internal file manager for the Noir project. + manager: FileManager, + + /// The root file name for the project. + root_file_name: PathBuf, + + /// The files that were explicitly added to the compilation project. + /// + /// Namely, this will contain the file IDs for files added manually during + /// extraction tool execution, and not identifiers for files in the standard + /// library and other implicit libraries. + known_files: KnownFiles, +} + +impl Project { + /// Creates a new project with the provided root. + #[allow(clippy::missing_panics_doc)] + pub fn new(root: impl Into, root_file: Source) -> Self { + let root = root.into(); + let manager = file_manager_with_stdlib(&root); + let root_file_name = root_file.name.clone(); + let file_ids = KnownFiles::new(); + + let mut project = Self { + manager, + root_file_name, + known_files: file_ids, + }; + + // The panic should be impossible. + project + .add_source(root_file) + .expect("The project has been newly created, so we can always add the root file."); + + project + } + + /// Adds the provided `source` to the Noir project. + /// + /// # Errors + /// + /// - [`FileError::DuplicateFile`] if the provided file already exists in + /// the project. + pub fn add_source(&mut self, source: Source) -> FileResult<()> { + let file_id = self + .manager + .add_file_with_source(source.name.as_path(), source.contents) + .ok_or(FileError::DuplicateFile(source.name))?; + + self.known_files.insert(file_id); + + Ok(()) + } + + /// Adds the provided `sources` to the Noir project. + /// + /// # Errors + /// + /// - [`FileError::DuplicateFile`] if any of the provided sources already + /// exists in the project. + pub fn add_sources(&mut self, sources: impl Iterator) -> FileResult<()> { + for source in sources { + self.add_source(source)?; + } + + Ok(()) + } + + /// Gets the root file of the project as a Path. + #[must_use] + pub fn root_file(&self) -> &Path { + self.root_file_name.as_path() + } + + /// Takes the project definition and performs compilation of that project to + /// the Noir intermediate representation for further analysis and the + /// emission of Lean code. + /// + /// If the compilation process generates non-fatal warnings, these are + /// attached to the return value. + /// + /// # Errors + /// + /// - [`CompileError`] if the compilation process fails. + pub fn compile(self) -> CompileResult> { + // Grab all required fields from `self`. + let root_path = self.root_file_name; + let manager = self.manager; + let known_files = self.known_files; + + // Start by parsing the files that the file manager knows about. + let parsed_files = parse_all(&manager); + + // Then we build our compilation context + let mut context = Context::new(manager, parsed_files); + context.track_references(); + let root_crate = prepare_crate(&mut context, root_path.as_path()); + + // Perform compilation to check the code within it. + let ((), warnings) = check_crate(&mut context, root_crate, false, false, None) + .map_err(|diagnostics| CompileError::CheckFailure { diagnostics })?; + + Ok(WithWarnings::new( + LeanEmitter::new(context, known_files, root_crate), + warnings, + )) + } +} + +impl From for FileManager { + fn from(value: Project) -> Self { + value.manager + } +} diff --git a/src/noir/source.rs b/src/noir/source.rs new file mode 100644 index 0000000..4387af4 --- /dev/null +++ b/src/noir/source.rs @@ -0,0 +1,41 @@ +//! A representation of an unparsed Noir source. + +use std::{fs::File, io::Read, path::PathBuf}; + +use crate::error::file::{Error, Result}; + +/// An unparsed Noir source file. +#[derive(Clone, Debug, PartialEq, PartialOrd)] +pub struct Source { + /// The name of the source file. + pub name: PathBuf, + + /// The contents of the source file. + pub contents: String, +} + +impl Source { + /// Create a new source from a file path and contents. + pub fn new(path: impl Into, contents: impl Into) -> Self { + let name = path.into(); + let contents = contents.into(); + + Self { name, contents } + } + + /// Creates a new source file by reading the file at the specified path to + /// get the contents of the file. + /// + /// # Errors + /// + /// - [`Error::MissingFile`] if the provided file cannot be read. + pub fn read(path: impl Into) -> Result { + let name = path.into(); + let mut file = File::open(&name).map_err(|_| Error::MissingFile(name.clone()))?; + let mut contents = String::new(); + file.read_to_string(&mut contents) + .map_err(|_| Error::MissingFile(name.clone()))?; + + Ok(Self { name, contents }) + } +}