my-project-public

repository

loading code, commits, and activity

repositories

loading repo index

my-project-public — gitlawb

#1	use anyhow::{Context, Result};
#2	use std::fs;
#3	use std::path::{Path, PathBuf};
#4
#5	const CONSOLIDATED_LAKEFILE: &str = r#"import Lake
#6	open Lake DSL
#7
#8	package escrowProofs
#9
#10	require mathlib from git
#11	"https://github.com/leanprover-community/mathlib4.git" @ "v4.15.0"
#12	require qedgenSupport from
#13	"./lean_support"
#14
#15	@[default_target]
#16	lean_lib EscrowProofs where
#17	roots := #[`EscrowProofs]
#18	"#;
#19
#20	const CONSOLIDATED_README: &str = r#"# Solana Program Lean Proofs
#21
#22	This directory contains formal verification proofs for the Solana program, generated using QEDGen.
#23
#24	## Building and Verifying
#25
#26	To build and verify all proofs:
#27
#28	```bash
#29	lake build
#30	```
#31
#32	This will verify all theorems and ensure they compile correctly.
#33
#34	## Structure
#35
#36	All proofs are contained in `EscrowProofs.lean`, organized into namespaces to avoid naming conflicts:
#37	- Each proof has its own namespace
#38	- Shared definitions from the QEDGen Solana library are imported at the top
#39	- The `lean_support` directory contains the Solana modeling framework
#40
#41	## Generated Proofs
#42
#43	See `EscrowProofs.lean` for the complete list of theorems and their proofs.
#44	"#;
#45
#46	const CONSOLIDATED_GITIGNORE: &str = r#"/.lake
#47	/lake-manifest.json
#48	/lakefile.olean
#49	/lakefile.olean.trace
#50	*.olean
#51	*.trace
#52	.lake
#53	"#;
#54
#55	/// Find all Best.lean files in subdirectories of the given path
#56	fn find_proof_files(input_dir: &Path) -> Result<Vec<PathBuf>> {
#57	let mut proof_files = Vec::new();
#58
#59	if !input_dir.is_dir() {
#60	anyhow::bail!("Input path is not a directory: {}", input_dir.display());
#61	}
#62
#63	for entry in fs::read_dir(input_dir)? {
#64	let entry = entry?;
#65	let path = entry.path();
#66
#67	if path.is_dir() {
#68	let best_lean = path.join("Best.lean");
#69	if best_lean.exists() {
#70	proof_files.push(best_lean);
#71	}
#72	}
#73	}
#74
#75	if proof_files.is_empty() {
#76	anyhow::bail!("No Best.lean files found in subdirectories of {}", input_dir.display());
#77	}
#78
#79	proof_files.sort();
#80	Ok(proof_files)
#81	}
#82
#83	/// Extract namespace from directory name (e.g., "cancel_access_control" -> "CancelAccessControl")
#84	fn to_namespace(dir_name: &str) -> String {
#85	dir_name
#86	.split('_')
#87	.map(\|word\| {
#88	let mut chars = word.chars();
#89	match chars.next() {
#90	None => String::new(),
#91	Some(first) => first.to_uppercase().collect::<String>() + chars.as_str(),
#92	}
#93	})
#94	.collect()
#95	}
#96
#97	/// Read a proof file, extract its imports, and wrap the body in a namespace
#98	fn process_proof_file(proof_file: &Path) -> Result<(String, Vec<String>, String)> {
#99	let content = fs::read_to_string(proof_file)
#100	.with_context(\|\| format!("Failed to read {}", proof_file.display()))?;
#101
#102	let parent = proof_file
#103	.parent()
#104	.and_then(\|p\| p.file_name())
#105	.and_then(\|n\| n.to_str())
#106	.ok_or_else(\|\| anyhow::anyhow!("Could not determine parent directory"))?;
#107
#108	let namespace = to_namespace(parent);
#109
#110	// Collect imports and find where the body starts
#111	let lines: Vec<&str> = content.lines().collect();
#112	let mut imports = Vec::new();
#113	let mut content_start = 0;
#114
#115	for (i, line) in lines.iter().enumerate() {
#116	let trimmed = line.trim();
#117	if trimmed.starts_with("import ") {
#118	imports.push(trimmed.to_string());
#119	} else if !trimmed.is_empty() && !trimmed.starts_with("open ") && !trimmed.starts_with("--") {
#120	content_start = i;
#121	break;
#122	}
#123	}
#124
#125	// Skip any remaining open/empty lines
#126	while content_start < lines.len() {
#127	let trimmed = lines[content_start].trim();
#128	if !trimmed.is_empty() && !trimmed.starts_with("open ") {
#129	break;
#130	}
#131	content_start += 1;
#132	}
#133
#134	let proof_content = lines[content_start..].join("\n");
#135
#136	Ok((namespace, imports, proof_content))
#137	}
#138
#139	/// Consolidate multiple Lean proof projects into a single project
#140	pub fn consolidate_proofs(input_dir: &Path, output_dir: &Path) -> Result<()> {
#141	// Create output directory
#142	fs::create_dir_all(output_dir)?;
#143
#144	// Find all proof files
#145	let proof_files = find_proof_files(input_dir)?;
#146	println!("Found {} proof files to consolidate", proof_files.len());
#147
#148	// Process all proof files and collect their imports
#149	let mut all_imports = std::collections::BTreeSet::new();
#150	let mut proofs = Vec::new();
#151
#152	for proof_file in &proof_files {
#153	let (namespace, imports, content) = process_proof_file(proof_file)?;
#154	all_imports.extend(imports);
#155	proofs.push((namespace, content));
#156	}
#157
#158	// Build the consolidated proof file
#159	let mut consolidated = String::new();
#160
#161	// Add union of all imports
#162	for import in &all_imports {
#163	consolidated.push_str(import);
#164	consolidated.push('\n');
#165	}
#166	consolidated.push_str("\nopen QEDGen.Solana\n\n");
#167
#168	// Write each proof in its namespace
#169	for (namespace, content) in &proofs {
#170
#171	consolidated.push_str(&format!(
#172	"/- {separator}\n {title}\n {separator} -/\n\n",
#173	separator = "=".repeat(76),
#174	title = format!("{} Proof", namespace)
#175	));
#176
#177	consolidated.push_str(&format!("namespace {}\n\n", namespace));
#178	consolidated.push_str(&content);
#179	consolidated.push_str("\n\nend ");
#180	consolidated.push_str(&namespace);
#181	consolidated.push_str("\n\n");
#182	}
#183
#184	// Write the consolidated proof file
#185	fs::write(output_dir.join("EscrowProofs.lean"), consolidated)?;
#186
#187	// Copy lean_support from one of the proof directories
#188	let first_proof_dir = proof_files[0].parent().unwrap();
#189	let source_support = first_proof_dir.join("lean_support");
#190	let dest_support = output_dir.join("lean_support");
#191
#192	if source_support.exists() {
#193	copy_dir_recursive(&source_support, &dest_support)?;
#194	}
#195
#196	// Copy lean-toolchain
#197	let source_toolchain = first_proof_dir.join("lean-toolchain");
#198	if source_toolchain.exists() {
#199	fs::copy(&source_toolchain, output_dir.join("lean-toolchain"))?;
#200	}
#201
#202	// Write lakefile, README, and .gitignore
#203	fs::write(output_dir.join("lakefile.lean"), CONSOLIDATED_LAKEFILE)?;
#204	fs::write(output_dir.join("README.md"), CONSOLIDATED_README)?;
#205	fs::write(output_dir.join(".gitignore"), CONSOLIDATED_GITIGNORE)?;
#206
#207	println!("Consolidated proofs written to {}", output_dir.display());
#208	println!(" - EscrowProofs.lean");
#209	println!(" - lakefile.lean");
#210	println!(" - lean-toolchain");
#211	println!(" - lean_support/");
#212	println!(" - README.md");
#213	println!(" - .gitignore");
#214
#215	Ok(())
#216	}
#217
#218	/// Recursively copy a directory
#219	fn copy_dir_recursive(src: &Path, dst: &Path) -> Result<()> {
#220	if !dst.exists() {
#221	fs::create_dir_all(dst)?;
#222	}
#223
#224	for entry in fs::read_dir(src)? {
#225	let entry = entry?;
#226	let path = entry.path();
#227	let dest_path = dst.join(entry.file_name());
#228
#229	if path.is_dir() {
#230	copy_dir_recursive(&path, &dest_path)?;
#231	} else {
#232	fs::copy(&path, &dest_path)?;
#233	}
#234	}
#235
#236	Ok(())
#237	}
#238

z6Mkq5mY3JWtxoxUobWcfNHm7AkRubgSWEZTkBVqZXJviFZ5/my-project-public