diff --git a/analysis/src/lib.rs b/analysis/src/lib.rs index 641fd9bb8..adb7a1c7a 100644 --- a/analysis/src/lib.rs +++ b/analysis/src/lib.rs @@ -11,7 +11,7 @@ pub fn convert_asm_to_pil( ) -> Result, Vec> { let mut monitor = DiffMonitor::default(); let file = analyze(file, &mut monitor)?; - Ok(convert_analyzed_to_pil_constraints(file, &mut monitor)) + Ok(convert_vms_to_constrained(file, &mut monitor)) } pub fn analyze( @@ -23,7 +23,7 @@ pub fn analyze( let file = type_check::check(file)?; monitor.push(&file); - // run analysis on virtual machines, reducing them to constrained machines + // run analysis on virtual machines, batching instructions log::debug!("Start asm analysis"); let file = vm::analyze(file, monitor)?; log::debug!("End asm analysis"); @@ -31,7 +31,9 @@ pub fn analyze( Ok(file) } -pub fn convert_analyzed_to_pil_constraints( +/// Converts all VMs to constrained machines, replacing +/// assembly instructions by lookups to programs. +pub fn convert_vms_to_constrained( file: AnalysisASMFile, monitor: &mut DiffMonitor, ) -> AnalysisASMFile { @@ -62,11 +64,11 @@ pub mod utils { #[cfg(test)] mod test_util { use ast::asm_analysis::AnalysisASMFile; - use importer::resolve_str; + use importer::load_dependencies_and_resolve_str; use number::FieldElement; /// A test utility to process a source file until after type checking pub fn typecheck_str(source: &str) -> Result, Vec> { - type_check::check(resolve_str(source)) + type_check::check(load_dependencies_and_resolve_str(source)) } } diff --git a/compiler/benches/executor_benchmark.rs b/compiler/benches/executor_benchmark.rs index 20fb1aa8c..ffa207321 100644 --- a/compiler/benches/executor_benchmark.rs +++ b/compiler/benches/executor_benchmark.rs @@ -33,7 +33,7 @@ fn criterion_benchmark(c: &mut Criterion) { b.iter(|| { run_witgen( &pil_with_constants.pil, - pil_with_constants.constants.clone(), + pil_with_constants.fixed_cols.clone(), ) }) }); diff --git a/compiler/src/pipeline.rs b/compiler/src/pipeline.rs index 765b7c312..b81e76458 100644 --- a/compiler/src/pipeline.rs +++ b/compiler/src/pipeline.rs @@ -6,7 +6,6 @@ use std::{ time::Instant, }; -use analysis::convert_analyzed_to_pil_constraints; use ast::{ analyzed::Analyzed, asm_analysis::AnalysisASMFile, @@ -34,9 +33,9 @@ pub struct GeneratedWitness { pub witness: Option)>>, } -pub struct PilWithConstants { +pub struct PilWithEvaluatedFixedCols { pub pil: Analyzed, - pub constants: Vec<(String, Vec)>, + pub fixed_cols: Vec<(String, Vec)>, } pub struct ProofResult { @@ -52,51 +51,54 @@ pub struct ProofResult { #[derive(Debug, PartialEq, Eq, Clone, Copy)] pub enum Stage { - AsmFile, + AsmFilePath, AsmString, - Parsed, - Resolved, + ParsedAsmFile, + ResolvedModuleTree, AnalyzedAsm, - PilConstraints, - Graph, - Linked, - PilFile, + ConstrainedMachineCollection, + LinkedMachineGraph, + ParsedPilFile, + PilFilePath, PilString, AnalyzedPil, OptimizedPil, - PilWithConstants, + PilWithEvaluatedFixedCols, GeneratedWitness, Proof, } enum Artifact { - /// The path to the .asm file. - AsmFile(PathBuf), - /// The contents of the .asm file, with an optional Path (for error messages). + /// The path to a single .asm file. + AsmFilePath(PathBuf), + /// The contents of a single .asm file, with an optional Path (for imports). AsmString(Option, String), - /// The parsed .asm file, with an optional Path (for error messages). - Parsed(Option, ASMProgram), - /// The resolved .asm file. - Resolved(ASMProgram), - /// The analyzed .asm file. + /// A parsed .asm file, with an optional Path (for imports). + ParsedAsmFile(Option, ASMProgram), + /// A tree of .asm modules (with all dependencies potentially imported + /// from other files) with all references resolved to absolute symbol paths. + ResolvedModuleTree(ASMProgram), + /// The analyzed .asm file: Assignment registers are inferred, instructions + /// are batched and some properties are checked. AnalyzedAsm(AnalysisASMFile), - /// The pil constraints. - PilConstraints(AnalysisASMFile), - /// The airgen graph. - Graph(PILGraph), - /// The linked pil. - Linked(PILFile), - /// The path to the .pil file. - PilFile(PathBuf), - /// The contents of the .pil file. + /// A machine collection that only contains constrained machines. + ConstrainedMachineCollection(AnalysisASMFile), + /// The airgen graph, i.e. a collection of constrained machines with resolved + /// links between them. + LinkedMachineGraph(PILGraph), + /// A single parsed pil file. + ParsedPilFile(PILFile), + /// The path to a single .pil file. + PilFilePath(PathBuf), + /// The contents of a single .pil file. PilString(String), - /// The analyzed .pil file. - AnaylyzedPil(Analyzed), - /// The optimized .pil file. + /// An analyzed .pil file, with all dependencies imported, potentially from other files. + AnalyzedPil(Analyzed), + /// An optimized .pil file. OptimzedPil(Analyzed), - /// The optimized .pil file with constants. - PilWithConstants(PilWithConstants), - /// The generated witness. + /// An optimized .pil file with fixed columns fully evaluated. + PilWithEvaluatedFixedCols(PilWithEvaluatedFixedCols), + /// Generated witnesses including fixed columns and the corresponding PIL file. GeneratedWitness(GeneratedWitness), /// The proof (if successful) Proof(ProofResult), @@ -167,19 +169,19 @@ where /// The pipeline steps are: /// ```mermaid /// graph TD -/// AsmFile --> AsmString +/// AsmFilePath --> AsmString /// AsmString --> Parsed -/// Parsed --> Resolved -/// Resolved --> AnalyzedAsm -/// AnalyzedAsm --> PilConstraints -/// PilConstraints --> Graph -/// Graph --> Linked -/// Linked --> AnaylyzedPil -/// PilFile --> AnaylyzedPil -/// PilString --> AnaylyzedPil -/// AnaylyzedPil --> OptimzedPil -/// OptimzedPil --> PilWithConstants -/// PilWithConstants --> GeneratedWitness +/// ParsedAsmFile --> ResolvedModuleTree +/// ResolvedModuleTree --> AnalyzedAsm +/// AnalyzedAsm --> ConstrainedMachineCollection +/// ConstrainedMachineCollection --> LinkedMachineGraph +/// LinkedMachineGraph --> ParsedPilFile +/// ParsedPilFile --> AnalyzedPil +/// PilFilePath --> AnalyzedPil +/// PilString --> AnalyzedPil +/// AnalyzedPil --> OptimzedPil +/// OptimzedPil --> PilWithEvaluatedFixedCols +/// PilWithEvaluatedFixedCols --> GeneratedWitness /// GeneratedWitness --> Proof /// ``` /// @@ -292,7 +294,7 @@ impl Pipeline { pub fn from_asm_file(self, asm_file: PathBuf) -> Self { let name = self.name.or(Some(Self::name_from_path(&asm_file))); Pipeline { - artifact: Some(Artifact::AsmFile(asm_file)), + artifact: Some(Artifact::AsmFilePath(asm_file)), name, ..self } @@ -310,7 +312,7 @@ impl Pipeline { pub fn from_pil_file(self, pil_file: PathBuf) -> Self { let name = self.name.or(Some(Self::name_from_path(&pil_file))); Pipeline { - artifact: Some(Artifact::PilFile(pil_file)), + artifact: Some(Artifact::PilFilePath(pil_file)), name, ..self } @@ -361,7 +363,7 @@ impl Pipeline { fn advance(&mut self) -> Result<(), Vec> { let artifact = std::mem::take(&mut self.artifact).unwrap(); self.artifact = Some(match artifact { - Artifact::AsmFile(path) => Artifact::AsmString( + Artifact::AsmFilePath(path) => Artifact::AsmString( Some(path.clone()), fs::read_to_string(&path).map_err(|e| { vec![format!("Error reading .asm file: {}\n{e}", path.display())] @@ -377,56 +379,58 @@ impl Pipeline { panic!(); }); self.diff_monitor.push(&parsed_asm); - Artifact::Parsed(path, parsed_asm) + Artifact::ParsedAsmFile(path, parsed_asm) } - Artifact::Parsed(path, parsed) => { - self.log("Resolve imports"); - let resolved = importer::resolve(path, parsed).map_err(|e| vec![e])?; + Artifact::ParsedAsmFile(path, parsed) => { + self.log("Loading dependencies and resolving references"); + let resolved = + importer::load_dependencies_and_resolve(path, parsed).map_err(|e| vec![e])?; self.diff_monitor.push(&resolved); - Artifact::Resolved(resolved) + Artifact::ResolvedModuleTree(resolved) } - Artifact::Resolved(resolved) => { + Artifact::ResolvedModuleTree(resolved) => { self.log("Run analysis"); - self.log("Analysis done"); let analyzed_asm = analysis::analyze(resolved, &mut self.diff_monitor)?; + self.log("Analysis done"); log::trace!("{analyzed_asm}"); Artifact::AnalyzedAsm(analyzed_asm) } - Artifact::AnalyzedAsm(analyzed_asm) => Artifact::PilConstraints( - convert_analyzed_to_pil_constraints(analyzed_asm, &mut self.diff_monitor), + Artifact::AnalyzedAsm(analyzed_asm) => Artifact::ConstrainedMachineCollection( + analysis::convert_vms_to_constrained(analyzed_asm, &mut self.diff_monitor), ), - Artifact::PilConstraints(analyzed_asm) => { + Artifact::ConstrainedMachineCollection(analyzed_asm) => { self.log("Run airgen"); let graph = airgen::compile(analyzed_asm); self.diff_monitor.push(&graph); self.log("Airgen done"); log::trace!("{graph}"); - Artifact::Graph(graph) + Artifact::LinkedMachineGraph(graph) } - Artifact::Graph(graph) => { + Artifact::LinkedMachineGraph(graph) => { self.log("Run linker"); let linked = linker::link(graph)?; self.diff_monitor.push(&linked); log::trace!("{linked}"); self.maybe_write_pil(&linked, "")?; - Artifact::Linked(linked) + Artifact::ParsedPilFile(linked) } - Artifact::Linked(linked) => { - // TODO: We should probably offer a way to analyze a PILFile directly + Artifact::ParsedPilFile(linked) => { + // TODO: We should probably offer a way to analyze a PILFile directly, + // i.e. without going through a string. self.log("Materialize linked file"); let linked = format!("{linked}"); - self.log("Anylyzing pil..."); - Artifact::AnaylyzedPil(pil_analyzer::analyze_string(&linked)) + self.log("Analyzing pil..."); + Artifact::AnalyzedPil(pil_analyzer::analyze_string(&linked)) } - Artifact::PilFile(pil_file) => { - self.log("Anylyzing pil..."); - Artifact::AnaylyzedPil(pil_analyzer::analyze(&pil_file)) + Artifact::PilFilePath(pil_file) => { + self.log("Analyzing pil..."); + Artifact::AnalyzedPil(pil_analyzer::analyze(&pil_file)) } Artifact::PilString(pil_string) => { - self.log("Anylyzing pil..."); - Artifact::AnaylyzedPil(pil_analyzer::analyze_string(&pil_string)) + self.log("Analyzing pil..."); + Artifact::AnalyzedPil(pil_analyzer::analyze_string(&pil_string)) } - Artifact::AnaylyzedPil(analyzed_pil) => { + Artifact::AnalyzedPil(analyzed_pil) => { self.log("Optimizing pil..."); let optimized = pilopt::optimize(analyzed_pil); self.maybe_write_pil(&optimized, "_opt")?; @@ -435,17 +439,17 @@ impl Pipeline { Artifact::OptimzedPil(pil) => { self.log("Evaluating fixed columns..."); let start = Instant::now(); - let constants = constant_evaluator::generate(&pil); - let constants = constants + let fixed_cols = constant_evaluator::generate(&pil); + let fixed_cols = fixed_cols .into_iter() .map(|(k, v)| (k.to_string(), v)) .collect::>(); - self.maybe_write_constants(&constants)?; + self.maybe_write_constants(&fixed_cols)?; self.log(&format!("Took {}", start.elapsed().as_secs_f32())); - Artifact::PilWithConstants(PilWithConstants { pil, constants }) + Artifact::PilWithEvaluatedFixedCols(PilWithEvaluatedFixedCols { pil, fixed_cols }) } - Artifact::PilWithConstants(PilWithConstants { pil, constants }) => { - let witness = (pil.constant_count() == constants.len()).then(|| { + Artifact::PilWithEvaluatedFixedCols(PilWithEvaluatedFixedCols { pil, fixed_cols }) => { + let witness = (pil.constant_count() == fixed_cols.len()).then(|| { self.log("Deducing witness columns..."); let start = Instant::now(); let external_witness_values = @@ -456,7 +460,7 @@ impl Pipeline { .take() .unwrap_or_else(|| Box::new(executor::witgen::unused_query_callback())); let witness = - executor::witgen::WitnessGenerator::new(&pil, &constants, query_callback) + executor::witgen::WitnessGenerator::new(&pil, &fixed_cols, query_callback) .with_external_witness_values(external_witness_values) .generate(); @@ -467,10 +471,10 @@ impl Pipeline { .collect::>() }); - self.maybe_write_witness(&constants, &witness)?; + self.maybe_write_witness(&fixed_cols, &witness)?; Artifact::GeneratedWitness(GeneratedWitness { pil, - constants, + constants: fixed_cols, witness, }) } @@ -627,19 +631,19 @@ impl Pipeline { fn stage(&self) -> Stage { match self.artifact.as_ref().unwrap() { - Artifact::AsmFile(_) => Stage::AsmFile, + Artifact::AsmFilePath(_) => Stage::AsmFilePath, Artifact::AsmString(_, _) => Stage::AsmString, - Artifact::Parsed(_, _) => Stage::Parsed, - Artifact::Resolved(_) => Stage::Resolved, + Artifact::ParsedAsmFile(_, _) => Stage::ParsedAsmFile, + Artifact::ResolvedModuleTree(_) => Stage::ResolvedModuleTree, Artifact::AnalyzedAsm(_) => Stage::AnalyzedAsm, - Artifact::PilConstraints(_) => Stage::PilConstraints, - Artifact::Graph(_) => Stage::Graph, - Artifact::Linked(_) => Stage::Linked, - Artifact::PilFile(_) => Stage::PilFile, + Artifact::ConstrainedMachineCollection(_) => Stage::ConstrainedMachineCollection, + Artifact::LinkedMachineGraph(_) => Stage::LinkedMachineGraph, + Artifact::ParsedPilFile(_) => Stage::ParsedPilFile, + Artifact::PilFilePath(_) => Stage::PilFilePath, Artifact::PilString(_) => Stage::PilString, - Artifact::AnaylyzedPil(_) => Stage::AnalyzedPil, + Artifact::AnalyzedPil(_) => Stage::AnalyzedPil, Artifact::OptimzedPil(_) => Stage::OptimizedPil, - Artifact::PilWithConstants(_) => Stage::PilWithConstants, + Artifact::PilWithEvaluatedFixedCols(_) => Stage::PilWithEvaluatedFixedCols, Artifact::GeneratedWitness(_) => Stage::GeneratedWitness, Artifact::Proof(_) => Stage::Proof, } @@ -684,9 +688,11 @@ impl Pipeline { Ok(optimized_pil) } - pub fn optimized_pil_with_constants(mut self) -> Result, Vec> { - self.advance_to(Stage::PilWithConstants)?; - let Artifact::PilWithConstants(pil_with_constants) = self.artifact.unwrap() else { + pub fn optimized_pil_with_constants( + mut self, + ) -> Result, Vec> { + self.advance_to(Stage::PilWithEvaluatedFixedCols)?; + let Artifact::PilWithEvaluatedFixedCols(pil_with_constants) = self.artifact.unwrap() else { panic!() }; Ok(pil_with_constants) diff --git a/importer/src/lib.rs b/importer/src/lib.rs index 24f2ee214..0d440a5c2 100644 --- a/importer/src/lib.rs +++ b/importer/src/lib.rs @@ -13,7 +13,7 @@ use parser::parse_asm; use path_canonicalizer::canonicalize_paths; use powdr_std::add_std; -pub fn resolve( +pub fn load_dependencies_and_resolve( path: Option, module: ASMProgram, ) -> Result, String> { @@ -23,6 +23,6 @@ pub fn resolve( } /// A test utility to process a source file until after import resolution -pub fn resolve_str(source: &str) -> ASMProgram { - resolve(None, parse_asm(None, source).unwrap()).unwrap() +pub fn load_dependencies_and_resolve_str(source: &str) -> ASMProgram { + load_dependencies_and_resolve(None, parse_asm(None, source).unwrap()).unwrap() } diff --git a/linker/src/lib.rs b/linker/src/lib.rs index a915bdd61..ff9ba1286 100644 --- a/linker/src/lib.rs +++ b/linker/src/lib.rs @@ -161,7 +161,7 @@ mod test { fn parse_analyse_and_compile(input: &str) -> PILGraph { let parsed = parse_asm(None, input).unwrap(); - let resolved = importer::resolve(None, parsed).unwrap(); + let resolved = importer::load_dependencies_and_resolve(None, parsed).unwrap(); airgen::compile(convert_asm_to_pil(resolved).unwrap()) } diff --git a/riscv_executor/src/lib.rs b/riscv_executor/src/lib.rs index 27062136d..a34d903e8 100644 --- a/riscv_executor/src/lib.rs +++ b/riscv_executor/src/lib.rs @@ -888,7 +888,7 @@ pub fn execute( log::info!("Parsing..."); let parsed = parser::parse_asm::(None, asm_source).unwrap(); log::info!("Resolving imports..."); - let resolved = importer::resolve(None, parsed).unwrap(); + let resolved = importer::load_dependencies_and_resolve(None, parsed).unwrap(); log::info!("Analyzing..."); let analyzed = analysis::analyze(resolved, &mut ast::DiffMonitor::default()).unwrap(); diff --git a/type_check/src/lib.rs b/type_check/src/lib.rs index f5c456931..7d30a7744 100644 --- a/type_check/src/lib.rs +++ b/type_check/src/lib.rs @@ -340,7 +340,7 @@ impl TypeChecker { #[cfg(test)] mod tests { - use importer::resolve_str; + use importer::load_dependencies_and_resolve_str; use number::Bn254Field; use crate::check; @@ -348,7 +348,7 @@ mod tests { // A utility to test behavior of the type checker on source inputs // TODO: test returned values, not just success fn expect_check_str(src: &str, expected: Result<(), Vec<&str>>) { - let resolved = resolve_str::(src); + let resolved = load_dependencies_and_resolve_str::(src); let checked = check(resolved); assert_eq!( checked.map(|_| ()),