Merge pull request #1090 from AleoHQ/feature/cli-generates-proofs

Ast Proof Generation In CLI

ast/src/errors/ast.rs

@@ -0,0 +1,40 @@
+// Copyright (C) 2019-2021 Aleo Systems Inc.
+// This file is part of the Leo library.
+
+// The Leo library is free software: you can redistribute it and/or modify
+// it under the terms of the GNU General Public License as published by
+// the Free Software Foundation, either version 3 of the License, or
+// (at your option) any later version.
+
+// The Leo library is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+// GNU General Public License for more details.
+
+// You should have received a copy of the GNU General Public License
+// along with the Leo library. If not, see <https://www.gnu.org/licenses/>.
+
+use crate::{FormattedError, LeoError, ReducerError, Span};
+
+#[derive(Debug, Error)]
+pub enum AstError {
+    #[error("{}", _0)]
+    Error(#[from] FormattedError),
+
+    #[error("{}", _0)]
+    IOError(#[from] std::io::Error),
+
+    #[error("{}", _0)]
+    ReducerError(#[from] ReducerError),
+
+    #[error("{}", _0)]
+    SerdeJsonError(#[from] ::serde_json::Error),
+}
+
+impl LeoError for AstError {}
+
+impl AstError {
+    fn _new_from_span(message: String, span: &Span) -> Self {
+        AstError::Error(FormattedError::new_from_span(message, span))
+    }
+}

ast/src/errors/mod.rs

@@ -14,6 +14,9 @@
 // You should have received a copy of the GNU General Public License
 // along with the Leo library. If not, see <https://www.gnu.org/licenses/>.
 
+pub mod ast;
+pub use ast::*;
+
 pub mod canonicalization;
 pub use canonicalization::*;
 

ast/src/lib.rs

@@ -86,7 +86,7 @@ impl Ast {
     }
 
     /// Mutates the program ast by preforming canonicalization on it.
-    pub fn canonicalize(&mut self) -> Result<(), ReducerError> {
+    pub fn canonicalize(&mut self) -> Result<(), AstError> {
         self.ast = ReconstructingDirector::new(Canonicalizer::default()).reduce_program(self.as_repr())?;
         Ok(())
     }
@@ -101,12 +101,20 @@ impl Ast {
     }
 
     /// Serializes the ast into a JSON string.
-    pub fn to_json_string(&self) -> Result<String, serde_json::Error> {
-        serde_json::to_string_pretty(&self.ast)
+    pub fn to_json_string(&self) -> Result<String, AstError> {
+        Ok(serde_json::to_string_pretty(&self.ast)?)
+    }
+
+    pub fn to_json_file(&self, mut path: std::path::PathBuf, file_name: &str) -> Result<(), AstError> {
+        path.push(file_name);
+        let file = std::fs::File::create(path)?;
+        let writer = std::io::BufWriter::new(file);
+        serde_json::to_writer_pretty(writer, &self.ast)?;
+        Ok(())
     }
 
     /// Deserializes the JSON string into a ast.
-    pub fn from_json_string(json: &str) -> Result<Self, serde_json::Error> {
+    pub fn from_json_string(json: &str) -> Result<Self, AstError> {
         let ast: Program = serde_json::from_str(json)?;
         Ok(Self { ast })
     }

compiler/src/compiler.rs

@@ -15,7 +15,6 @@
 // along with the Leo library. If not, see <https://www.gnu.org/licenses/>.
 
 //! Compiles a Leo program from a file path.
-
 use crate::{
     constraints::{generate_constraints, generate_test_constraints},
     errors::CompilerError,
@@ -23,6 +22,8 @@ use crate::{
     GroupType,
     Output,
     OutputFile,
+    TheoremOptions,
+    TypeInferencePhase,
 };
 pub use leo_asg::{new_context, AsgContext as Context, AsgContext};
 use leo_asg::{Asg, AsgPass, FormattedError, Program as AsgProgram};
@@ -66,6 +67,7 @@ pub struct Compiler<'a, F: PrimeField, G: GroupType<F>> {
     context: AsgContext<'a>,
     asg: Option<AsgProgram<'a>>,
     options: CompilerOptions,
+    proof_options: TheoremOptions,
     _engine: PhantomData<F>,
     _group: PhantomData<G>,
 }
@@ -80,6 +82,7 @@ impl<'a, F: PrimeField, G: GroupType<F>> Compiler<'a, F, G> {
         output_directory: PathBuf,
         context: AsgContext<'a>,
         options: Option<CompilerOptions>,
+        proof_options: Option<TheoremOptions>,
     ) -> Self {
         Self {
             program_name: package_name.clone(),
@@ -90,6 +93,7 @@ impl<'a, F: PrimeField, G: GroupType<F>> Compiler<'a, F, G> {
             asg: None,
             context,
             options: options.unwrap_or_default(),
+            proof_options: proof_options.unwrap_or_default(),
             _engine: PhantomData,
             _group: PhantomData,
         }
@@ -108,8 +112,16 @@ impl<'a, F: PrimeField, G: GroupType<F>> Compiler<'a, F, G> {
         output_directory: PathBuf,
         context: AsgContext<'a>,
         options: Option<CompilerOptions>,
+        proof_options: Option<TheoremOptions>,
     ) -> Result<Self, CompilerError> {
-        let mut compiler = Self::new(package_name, main_file_path, output_directory, context, options);
+        let mut compiler = Self::new(
+            package_name,
+            main_file_path,
+            output_directory,
+            context,
+            options,
+            proof_options,
+        );
 
         compiler.parse_program()?;
 
@@ -139,8 +151,16 @@ impl<'a, F: PrimeField, G: GroupType<F>> Compiler<'a, F, G> {
         state_path: &Path,
         context: AsgContext<'a>,
         options: Option<CompilerOptions>,
+        proof_options: Option<TheoremOptions>,
     ) -> Result<Self, CompilerError> {
-        let mut compiler = Self::new(package_name, main_file_path, output_directory, context, options);
+        let mut compiler = Self::new(
+            package_name,
+            main_file_path,
+            output_directory,
+            context,
+            options,
+            proof_options,
+        );
 
         compiler.parse_input(input_string, input_path, state_string, state_path)?;
 
@@ -218,11 +238,19 @@ impl<'a, F: PrimeField, G: GroupType<F>> Compiler<'a, F, G> {
     pub fn parse_program_from_string(&mut self, program_string: &str) -> Result<(), CompilerError> {
         // Use the parser to construct the abstract syntax tree (ast).
 
-        let mut ast = parse_ast(self.main_file_path.to_str().unwrap_or_default(), program_string)?;
+        let mut ast: leo_ast::Ast = parse_ast(self.main_file_path.to_str().unwrap_or_default(), program_string)?;
+
+        if self.proof_options.initial {
+            ast.to_json_file(self.output_directory.clone(), "inital_ast.json")?;
+        }
 
         // Preform compiler optimization via canonicalizing AST if its enabled.
         if self.options.canonicalization_enabled {
             ast.canonicalize()?;
+
+            if self.proof_options.canonicalized {
+                ast.to_json_file(self.output_directory.clone(), "canonicalization_ast.json")?;
+            }
         }
 
         // Store the main program file.
@@ -238,6 +266,13 @@ impl<'a, F: PrimeField, G: GroupType<F>> Compiler<'a, F, G> {
             &mut leo_imports::ImportParser::new(self.main_file_path.clone()),
         )?;
 
+        if self.proof_options.type_inferenced {
+            let new_ast = TypeInferencePhase::default()
+                .phase_ast(&self.program, &asg.clone().into_repr())
+                .expect("Failed to produce type inference ast.");
+            new_ast.to_json_file(self.output_directory.clone(), "type_inferenced_ast.json")?;
+        }
+
         tracing::debug!("ASG generation complete");
 
         // Store the ASG.

compiler/src/errors/compiler.rs

@@ -16,7 +16,7 @@
 
 use crate::errors::{ExpressionError, FunctionError, ImportError, StatementError};
 use leo_asg::{AsgConvertError, FormattedError};
-use leo_ast::{LeoError, ReducerError};
+use leo_ast::{AstError, LeoError};
 use leo_input::InputParserError;
 use leo_parser::SyntaxError;
 use leo_state::LocalDataVerificationError;
@@ -62,7 +62,7 @@ pub enum CompilerError {
     AsgConvertError(#[from] AsgConvertError),
 
     #[error("{}", _0)]
-    ReducerError(#[from] ReducerError),
+    AstError(#[from] AstError),
 
     #[error("{}", _0)]
     StatementError(#[from] StatementError),

compiler/src/option.rs

@@ -36,3 +36,20 @@ impl Default for CompilerOptions {
         }
     }
 }
+
+#[derive(Clone)]
+pub struct TheoremOptions {
+    pub initial: bool,
+    pub canonicalized: bool,
+    pub type_inferenced: bool,
+}
+
+impl Default for TheoremOptions {
+    fn default() -> Self {
+        Self {
+            initial: false,
+            canonicalized: false,
+            type_inferenced: false,
+        }
+    }
+}

compiler/tests/mod.rs

@@ -52,7 +52,7 @@ fn new_compiler() -> EdwardsTestCompiler {
     let path = PathBuf::from("/test/src/main.leo");
     let output_dir = PathBuf::from(TEST_OUTPUT_DIRECTORY);
 
-    EdwardsTestCompiler::new(program_name, path, output_dir, make_test_context(), None)
+    EdwardsTestCompiler::new(program_name, path, output_dir, make_test_context(), None, None)
 }
 
 pub(crate) fn parse_program(program_string: &str) -> Result<EdwardsTestCompiler, CompilerError> {

compiler/tests/test.rs

@@ -40,7 +40,7 @@ fn new_compiler(path: PathBuf) -> EdwardsTestCompiler {
     let program_name = "test".to_string();
     let output_dir = PathBuf::from("/output/");
 
-    EdwardsTestCompiler::new(program_name, path, output_dir, make_test_context(), None)
+    EdwardsTestCompiler::new(program_name, path, output_dir, make_test_context(), None, None)
 }
 
 pub(crate) fn parse_program(program_string: &str) -> Result<EdwardsTestCompiler, CompilerError> {

leo/commands/build.rs

@@ -19,6 +19,7 @@ use leo_compiler::{
     compiler::{thread_leaked_context, Compiler},
     group::targets::edwards_bls12::EdwardsGroupType,
     CompilerOptions,
+    TheoremOptions,
 };
 use leo_package::{
     inputs::*,
@@ -43,6 +44,14 @@ pub struct BuildOptions {
     pub disable_code_elimination: bool,
     #[structopt(long, help = "Disable all compiler optimizations")]
     pub disable_all_optimizations: bool,
+    #[structopt(long, help = "Writes all theorem input AST files.")]
+    pub enable_all_theorems: bool,
+    #[structopt(long, help = "Writes AST files needed for the initial theorem before any changes.")]
+    pub enable_initial_theorem: bool,
+    #[structopt(long, help = "Writes AST files needed for canonicalization theorem.")]
+    pub enable_canonicalized_theorem: bool,
+    #[structopt(long, help = "Writes AST files needed for type inference theorem.")]
+    pub enable_type_inferenced_theorem: bool,
 }
 
 impl Default for BuildOptions {
@@ -51,6 +60,10 @@ impl Default for BuildOptions {
             disable_constant_folding: true,
             disable_code_elimination: true,
             disable_all_optimizations: true,
+            enable_all_theorems: false,
+            enable_initial_theorem: false,
+            enable_canonicalized_theorem: false,
+            enable_type_inferenced_theorem: false,
         }
     }
 }
@@ -73,6 +86,24 @@ impl From<BuildOptions> for CompilerOptions {
     }
 }
 
+impl From<BuildOptions> for TheoremOptions {
+    fn from(options: BuildOptions) -> Self {
+        if options.enable_all_theorems {
+            TheoremOptions {
+                initial: true,
+                canonicalized: true,
+                type_inferenced: true,
+            }
+        } else {
+            TheoremOptions {
+                initial: options.enable_initial_theorem,
+                canonicalized: options.enable_canonicalized_theorem,
+                type_inferenced: options.enable_type_inferenced_theorem,
+            }
+        }
+    }
+}
+
 /// Compile and build program command.
 #[derive(StructOpt, Debug)]
 #[structopt(setting = structopt::clap::AppSettings::ColoredHelp)]
@@ -141,6 +172,7 @@ impl Command for Build {
             &state_string,
             &state_path,
             thread_leaked_context(),
+            Some(self.compiler_options.clone().into()),
             Some(self.compiler_options.into()),
         )?;
 

leo/commands/test.rs

@@ -112,6 +112,7 @@ impl Command for Test {
                 output_directory.clone(),
                 thread_leaked_context(),
                 Some(self.compiler_options.clone().into()),
+                Some(self.compiler_options.clone().into()),
             )?;
 
             let temporary_program = program;