my-project-public

repository

loading code, commits, and activity

repositories

loading repo index

#1	mod api;
#2	mod consolidate;
#3	mod project;
#4	mod spec;
#5	mod validate;
#6
#7	use anyhow::Result;
#8	use clap::{Parser, Subcommand};
#9	use std::path::PathBuf;
#10
#11	/// CLI tool for formal Lean 4 verification of Solana programs
#12	#[derive(Parser)]
#13	#[command(name = "qedgen")]
#14	#[command(version, about, long_about = None)]
#15	struct Cli {
#16	#[command(subcommand)]
#17	command: Commands,
#18	}
#19
#20	#[derive(Subcommand)]
#21	enum Commands {
#22	/// Generate Lean 4 proofs using Leanstral API
#23	Generate {
#24	/// Path to prompt file
#25	#[arg(long)]
#26	prompt_file: PathBuf,
#27
#28	/// Directory to write generated Lean project
#29	#[arg(long)]
#30	output_dir: PathBuf,
#31
#32	/// Number of independent completions (pass@N)
#33	#[arg(long, default_value = "4")]
#34	passes: usize,
#35
#36	/// Sampling temperature
#37	#[arg(long, default_value = "0.6")]
#38	temperature: f64,
#39
#40	/// Max tokens per completion
#41	#[arg(long, default_value = "16384")]
#42	max_tokens: usize,
#43
#44	/// Validate completions with 'lake build Best'
#45	#[arg(long)]
#46	validate: bool,
#47	},
#48
#49	/// Fill sorry markers in a Lean file using Leanstral
#50	FillSorry {
#51	/// Path to Lean file containing sorry markers
#52	#[arg(long)]
#53	file: PathBuf,
#54
#55	/// Output path (default: overwrite input file)
#56	#[arg(long)]
#57	output: Option<PathBuf>,
#58
#59	/// Number of independent attempts per sorry
#60	#[arg(long, default_value = "3")]
#61	passes: usize,
#62
#63	/// Sampling temperature
#64	#[arg(long, default_value = "0.3")]
#65	temperature: f64,
#66
#67	/// Max tokens per completion
#68	#[arg(long, default_value = "16384")]
#69	max_tokens: usize,
#70
#71	/// Validate filled file with 'lake build'
#72	#[arg(long)]
#73	validate: bool,
#74	},
#75
#76	/// Generate a draft SPEC.md from an Anchor IDL
#77	Spec {
#78	/// Path to Anchor IDL JSON file
#79	#[arg(long)]
#80	idl: PathBuf,
#81
#82	/// Directory to write SPEC.md (default: ./formal_verification)
#83	#[arg(long, default_value = "./formal_verification")]
#84	output_dir: PathBuf,
#85	},
#86
#87	/// Consolidate multiple proof projects into a single Lean project
#88	Consolidate {
#89	/// Directory containing proof subdirectories (each with Best.lean)
#90	#[arg(long)]
#91	input_dir: PathBuf,
#92
#93	/// Directory to write consolidated Lean project
#94	#[arg(long)]
#95	output_dir: PathBuf,
#96	},
#97
#98	/// Set up the global validation workspace (scaffold + Mathlib cache)
#99	Setup {
#100	/// Directory for the validation workspace (default: platform cache dir)
#101	#[arg(long)]
#102	workspace: Option<PathBuf>,
#103	},
#104	}
#105
#106	#[tokio::main]
#107	async fn main() -> Result<()> {
#108	let cli = Cli::parse();
#109
#110	match cli.command {
#111	Commands::Generate {
#112	prompt_file,
#113	output_dir,
#114	passes,
#115	temperature,
#116	max_tokens,
#117	validate,
#118	} => {
#119	let prompt = std::fs::read_to_string(&prompt_file)?;
#120	api::generate_proofs(
#121	&prompt,
#122	&output_dir,
#123	passes,
#124	temperature,
#125	max_tokens,
#126	validate,
#127	None,
#128	)
#129	.await?;
#130	}
#131
#132	Commands::FillSorry {
#133	file,
#134	output,
#135	passes,
#136	temperature,
#137	max_tokens,
#138	validate,
#139	} => {
#140	api::fill_sorry(
#141	&file,
#142	output.as_deref(),
#143	passes,
#144	temperature,
#145	max_tokens,
#146	validate,
#147	)
#148	.await?;
#149	}
#150
#151	Commands::Spec { idl, output_dir } => {
#152	spec::generate_spec(&idl, &output_dir)?;
#153	}
#154
#155	Commands::Consolidate {
#156	input_dir,
#157	output_dir,
#158	} => {
#159	consolidate::consolidate_proofs(&input_dir, &output_dir)?;
#160	}
#161
#162	Commands::Setup { workspace } => {
#163	validate::setup_workspace(workspace.as_deref()).await?;
#164	}
#165	}
#166
#167	Ok(())
#168	}
#169

z6Mkq5mY3JWtxoxUobWcfNHm7AkRubgSWEZTkBVqZXJviFZ5/my-project-public