my-project-public

repository

loading code, commits, and activity

repositories

loading repo index

#1	// SPEC.md generator from Anchor IDL
#2	//
#3	// Reads the raw IDL JSON and generates a draft verification spec with:
#4	// - Security goals inferred from instruction patterns
#5	// - State model from IDL types
#6	// - Operations with pre/postconditions from instruction accounts/args
#7	// - Formal property skeletons
#8	// - Trust boundary
#9
#10	use anyhow::Result;
#11	use serde::Deserialize;
#12	use std::fmt::Write;
#13	use std::path::Path;
#14
#15	// ── IDL types (richer than analyzer's subset) ──────────────────────────────
#16
#17	#[derive(Debug, Deserialize)]
#18	struct Idl {
#19	metadata: IdlMetadata,
#20	#[serde(default)]
#21	instructions: Vec<IdlInstruction>,
#22	#[serde(default)]
#23	types: Vec<IdlTypeDef>,
#24	#[serde(default)]
#25	errors: Vec<IdlError>,
#26	}
#27
#28	#[derive(Debug, Deserialize)]
#29	struct IdlMetadata {
#30	name: String,
#31	}
#32
#33	#[derive(Debug, Deserialize)]
#34	struct IdlInstruction {
#35	name: String,
#36	#[serde(default)]
#37	docs: Vec<String>,
#38	#[serde(default)]
#39	accounts: Vec<IdlAccount>,
#40	#[serde(default)]
#41	args: Vec<IdlArg>,
#42	}
#43
#44	#[derive(Debug, Deserialize)]
#45	struct IdlAccount {
#46	name: String,
#47	#[serde(default)]
#48	signer: bool,
#49	#[serde(default)]
#50	writable: bool,
#51	#[serde(default)]
#52	pda: Option<IdlPda>,
#53	#[serde(default)]
#54	relations: Vec<String>,
#55	}
#56
#57	#[derive(Debug, Deserialize)]
#58	struct IdlPda {
#59	#[serde(default)]
#60	seeds: Vec<IdlSeed>,
#61	}
#62
#63	#[derive(Debug, Deserialize)]
#64	struct IdlSeed {
#65	#[serde(default)]
#66	#[allow(dead_code)]
#67	kind: String,
#68	#[serde(default)]
#69	value: Option<serde_json::Value>,
#70	#[serde(default)]
#71	path: Option<String>,
#72	}
#73
#74	#[derive(Debug, Deserialize)]
#75	struct IdlArg {
#76	name: String,
#77	#[serde(rename = "type")]
#78	ty: serde_json::Value,
#79	}
#80
#81	#[derive(Debug, Deserialize)]
#82	struct IdlTypeDef {
#83	name: String,
#84	#[serde(rename = "type")]
#85	ty: IdlTypeBody,
#86	}
#87
#88	#[derive(Debug, Deserialize)]
#89	struct IdlTypeBody {
#90	#[serde(default)]
#91	kind: String,
#92	#[serde(default)]
#93	fields: Vec<IdlField>,
#94	}
#95
#96	#[derive(Debug, Deserialize)]
#97	struct IdlField {
#98	name: String,
#99	#[serde(rename = "type")]
#100	ty: serde_json::Value,
#101	}
#102
#103	#[derive(Debug, Deserialize)]
#104	struct IdlError {
#105	name: String,
#106	msg: String,
#107	}
#108
#109	// ── Inferred patterns ──────────────────────────────────────────────────────
#110
#111	struct InstructionAnalysis {
#112	name: String,
#113	display_name: String,
#114	docs: String,
#115	signers: Vec<String>,
#116	#[allow(dead_code)]
#117	writable_accounts: Vec<String>,
#118	#[allow(dead_code)]
#119	pda_accounts: Vec<String>,
#120	has_one_relations: Vec<(String, String)>, // (account, related_to)
#121	args: Vec<(String, String)>, // (name, type)
#122	has_token_program: bool,
#123	has_close_semantics: bool,
#124	has_numeric_args: bool,
#125	}
#126
#127	// ── Generator ──────────────────────────────────────────────────────────────
#128
#129	pub fn generate_spec(idl_path: &Path, output_path: &Path) -> Result<()> {
#130	let idl_source = std::fs::read_to_string(idl_path)?;
#131	let idl: Idl = serde_json::from_str(&idl_source)?;
#132
#133	let analyses: Vec<InstructionAnalysis> = idl.instructions.iter().map(analyze_instruction).collect();
#134	let spec = build_spec(&idl, &analyses);
#135
#136	std::fs::create_dir_all(output_path)?;
#137	std::fs::write(output_path.join("SPEC.md"), spec)?;
#138	println!("Wrote {}", output_path.join("SPEC.md").display());
#139
#140	Ok(())
#141	}
#142
#143	fn analyze_instruction(ix: &IdlInstruction) -> InstructionAnalysis {
#144	let signers: Vec<String> = ix.accounts.iter()
#145	.filter(\|a\| a.signer)
#146	.map(\|a\| a.name.clone())
#147	.collect();
#148
#149	let writable_accounts: Vec<String> = ix.accounts.iter()
#150	.filter(\|a\| a.writable)
#151	.map(\|a\| a.name.clone())
#152	.collect();
#153
#154	let pda_accounts: Vec<String> = ix.accounts.iter()
#155	.filter(\|a\| a.pda.is_some())
#156	.map(\|a\| a.name.clone())
#157	.collect();
#158
#159	let has_one_relations: Vec<(String, String)> = ix.accounts.iter()
#160	.flat_map(\|a\| a.relations.iter().map(move \|r\| (a.name.clone(), r.clone())))
#161	.collect();
#162
#163	let args: Vec<(String, String)> = ix.args.iter()
#164	.map(\|a\| (a.name.clone(), type_label(&a.ty)))
#165	.collect();
#166
#167	let has_token_program = ix.accounts.iter()
#168	.any(\|a\| a.name.contains("token_program"));
#169
#170	// Close semantics: non-init instruction with a writable PDA state account
#171	// and either has_one relations or no args (terminal operations typically take no args)
#172	let has_writable_pda = ix.accounts.iter()
#173	.any(\|a\| a.writable && a.pda.is_some());
#174	let has_relations = ix.accounts.iter()
#175	.any(\|a\| !a.relations.is_empty());
#176	let is_init = ix.name.contains("init");
#177	let has_close_semantics = has_writable_pda && !is_init && (has_relations \|\| ix.args.is_empty());
#178
#179	let has_numeric_args = args.iter()
#180	.any(\|(_, ty)\| ty.starts_with('u') \|\| ty.starts_with('i'));
#181
#182	InstructionAnalysis {
#183	name: ix.name.clone(),
#184	display_name: snake_to_title(&ix.name),
#185	docs: ix.docs.join(" ").trim().to_string(),
#186	signers,
#187	writable_accounts,
#188	pda_accounts,
#189	has_one_relations,
#190	args,
#191	has_token_program,
#192	has_close_semantics,
#193	has_numeric_args,
#194	}
#195	}
#196
#197	fn build_spec(idl: &Idl, analyses: &[InstructionAnalysis]) -> String {
#198	let mut s = String::new();
#199	let program_name = snake_to_title(&idl.metadata.name);
#200
#201	// Header
#202	writeln!(s, "# {} Verification Spec v1.0\n", program_name).unwrap();
#203
#204	// Program summary from instruction docs
#205	let doc_summary: Vec<String> = analyses.iter()
#206	.filter(\|a\| !a.docs.is_empty())
#207	.map(\|a\| format!("- {}: {}", a.display_name, a.docs))
#208	.collect();
#209	if !doc_summary.is_empty() {
#210	writeln!(s, "<!-- TODO: Replace with a 1-2 sentence summary in your own words -->\n").unwrap();
#211	for line in &doc_summary {
#212	writeln!(s, "{}", line).unwrap();
#213	}
#214	writeln!(s).unwrap();
#215	}
#216
#217	// §0 Security Goals
#218	writeln!(s, "## 0. Security Goals\n").unwrap();
#219	writeln!(s, "The program MUST provide the following properties:\n").unwrap();
#220
#221	let mut goal_num = 1;
#222
#223	// Access control goals
#224	let signers_instructions: Vec<&InstructionAnalysis> = analyses.iter()
#225	.filter(\|a\| !a.signers.is_empty())
#226	.collect();
#227	if !signers_instructions.is_empty() {
#228	let names: Vec<&str> = signers_instructions.iter().map(\|a\| a.display_name.as_str()).collect();
#229	writeln!(s, "{}. Authorization: Only authorized signers MAY execute {}. \
#230	Each operation MUST verify the signer matches the expected authority.",
#231	goal_num, names.join(", ")).unwrap();
#232	goal_num += 1;
#233	}
#234
#235	// CPI correctness goals
#236	let cpi_instructions: Vec<&InstructionAnalysis> = analyses.iter()
#237	.filter(\|a\| a.has_token_program)
#238	.collect();
#239	if !cpi_instructions.is_empty() {
#240	let names: Vec<&str> = cpi_instructions.iter().map(\|a\| a.display_name.as_str()).collect();
#241	writeln!(s, "{}. CPI parameter correctness: Token transfers in {} MUST pass \
#242	the correct program ID, source, destination, authority, and amount. \
#243	No transfer MAY route tokens to an unintended account.",
#244	goal_num, names.join(", ")).unwrap();
#245	goal_num += 1;
#246	}
#247
#248	// State machine goals
#249	let close_instructions: Vec<&InstructionAnalysis> = analyses.iter()
#250	.filter(\|a\| a.has_close_semantics)
#251	.collect();
#252	if !close_instructions.is_empty() {
#253	let names: Vec<&str> = close_instructions.iter().map(\|a\| a.display_name.as_str()).collect();
#254	writeln!(s, "{}. One-shot safety: After {} completes, the account MUST be closed \
#255	and MUST NOT be reusable.",
#256	goal_num, names.join(" or ")).unwrap();
#257	goal_num += 1;
#258	}
#259
#260	// Arithmetic goals
#261	let numeric_instructions: Vec<&InstructionAnalysis> = analyses.iter()
#262	.filter(\|a\| a.has_numeric_args)
#263	.collect();
#264	if !numeric_instructions.is_empty() {
#265	writeln!(s, "{}. Arithmetic bounds: Numeric parameters MUST NOT overflow during processing.",
#266	goal_num).unwrap();
#267	}
#268
#269	writeln!(s).unwrap();
#270
#271	// §1 State Model
#272	writeln!(s, "## 1. State Model\n").unwrap();
#273	for ty in &idl.types {
#274	if ty.ty.kind == "struct" {
#275	writeln!(s, "```").unwrap();
#276	writeln!(s, "{} {{", ty.name).unwrap();
#277	let max_name_len = ty.ty.fields.iter().map(\|f\| f.name.len()).max().unwrap_or(0);
#278	for field in &ty.ty.fields {
#279	writeln!(s, " {:<width$} {}", format!("{}:", field.name), type_label(&field.ty),
#280	width = max_name_len + 1).unwrap();
#281	}
#282	writeln!(s, "}}").unwrap();
#283	writeln!(s, "```\n").unwrap();
#284	}
#285	}
#286
#287	// PDA derivations
#288	// Extract PDAs from the raw IDL
#289	let mut seen_pdas = std::collections::HashSet::new();
#290	for ix in &idl.instructions {
#291	for acct in &ix.accounts {
#292	if let Some(pda) = &acct.pda {
#293	if seen_pdas.insert(acct.name.clone()) {
#294	let seeds: Vec<String> = pda.seeds.iter().map(\|seed\| {
#295	if let Some(path) = &seed.path {
#296	format!("{}", path)
#297	} else if let Some(serde_json::Value::Array(bytes)) = &seed.value {
#298	let values: Vec<u8> = bytes.iter()
#299	.filter_map(\|v\| v.as_u64().and_then(\|n\| u8::try_from(n).ok()))
#300	.collect();
#301	String::from_utf8(values).unwrap_or_else(\|_\| "const".into())
#302	} else {
#303	"const".into()
#304	}
#305	}).collect();
#306	writeln!(s, "`{}` is a PDA derived from `[\"{}\"]`.",
#307	acct.name, seeds.join("\", \"")).unwrap();
#308	}
#309	}
#310	}
#311	}
#312	writeln!(s).unwrap();
#313
#314	// Lifecycle
#315	let has_lifecycle = analyses.iter().any(\|a\| a.has_close_semantics);
#316	if has_lifecycle {
#317	writeln!(s, "### Lifecycle\n").unwrap();
#318	writeln!(s, "<!-- TODO: Describe the lifecycle states and transitions -->\n").unwrap();
#319	writeln!(s, "```").unwrap();
#320	let init = analyses.iter().find(\|a\| a.name.contains("init"));
#321	let terminals: Vec<&str> = analyses.iter()
#322	.filter(\|a\| a.has_close_semantics)
#323	.map(\|a\| a.name.as_str())
#324	.collect();
#325	if let Some(init_ix) = init {
#326	write!(s, "{} → [open]", init_ix.name).unwrap();
#327	for (i, t) in terminals.iter().enumerate() {
#328	if i == 0 {
#329	writeln!(s, " → {} → [closed]", t).unwrap();
#330	} else {
#331	writeln!(s, "{}→ {} → [closed]",
#332	" ".repeat(init_ix.name.len() + 12), t).unwrap();
#333	}
#334	}
#335	}
#336	writeln!(s, "```\n").unwrap();
#337	}
#338
#339	// §2 Operations
#340	writeln!(s, "## 2. Operations\n").unwrap();
#341	for (i, analysis) in analyses.iter().enumerate() {
#342	writeln!(s, "### 2.{} {}\n", i + 1, analysis.display_name).unwrap();
#343
#344	if !analysis.docs.is_empty() {
#345	writeln!(s, "{}\n", analysis.docs).unwrap();
#346	}
#347
#348	// Signers
#349	if !analysis.signers.is_empty() {
#350	writeln!(s, "Signers: {} (MUST sign)\n",
#351	analysis.signers.iter().map(\|s\| format!("`{}`", s)).collect::<Vec<_>>().join(", ")).unwrap();
#352	}
#353
#354	// Preconditions from errors, relations, args
#355	writeln!(s, "Preconditions:").unwrap();
#356	for (acct, rel) in &analysis.has_one_relations {
#357	writeln!(s, "- `{}` MUST match `{}.{}` (enforced by `has_one`)", rel, acct, rel).unwrap();
#358	}
#359	// Check if there are related errors
#360	for err in &idl.errors {
#361	// Heuristic: associate errors with instructions that have matching arg patterns
#362	let err_lower = err.name.to_lowercase();
#363	let args_lower: Vec<String> = analysis.args.iter().map(\|(n, _)\| n.to_lowercase()).collect();
#364	if args_lower.iter().any(\|a\| err_lower.contains(a)) \|\| err_lower.contains(&analysis.name.to_lowercase()) {
#365	writeln!(s, "- `{}`: {}", err.name, err.msg).unwrap();
#366	}
#367	}
#368	writeln!(s).unwrap();
#369
#370	// Effects
#371	writeln!(s, "Effects:").unwrap();
#372	let mut effect_num = 1;
#373	if analysis.has_token_program {
#374	// Find the corresponding IDL instruction for full account details
#375	if let Some(idl_ix) = idl.instructions.iter().find(\|i\| i.name == analysis.name) {
#376	let writable_token: Vec<&IdlAccount> = idl_ix.accounts.iter()
#377	.filter(\|a\| a.writable && a.name.contains("token") && !a.name.contains("program"))
#378	.collect();
#379	// Separate PDA vaults from user accounts
#380	let vaults: Vec<&&IdlAccount> = writable_token.iter().filter(\|a\| a.pda.is_some()).collect();
#381	let user_accounts: Vec<&&IdlAccount> = writable_token.iter().filter(\|a\| a.pda.is_none()).collect();
#382
#383	if analysis.name.contains("init") {
#384	// Init: user → vault
#385	for (u, v) in user_accounts.iter().zip(vaults.iter()) {
#386	writeln!(s, "{}. Transfer tokens: `{}` → `{}`",
#387	effect_num, u.name, v.name).unwrap();
#388	effect_num += 1;
#389	}
#390	} else if vaults.len() == 1 && user_accounts.len() == 1 {
#391	// Terminal with one transfer: vault → user (e.g., cancel)
#392	writeln!(s, "{}. Transfer tokens: `{}` → `{}`",
#393	effect_num, vaults[0].name, user_accounts[0].name).unwrap();
#394	effect_num += 1;
#395	} else {
#396	// Multiple transfers: list all writable token accounts as
#397	// TODO for the user to specify direction
#398	for pair in writable_token.chunks(2) {
#399	if pair.len() == 2 {
#400	writeln!(s, "{}. Transfer tokens: `{}` ↔ `{}` <!-- TODO: confirm direction -->",
#401	effect_num, pair[0].name, pair[1].name).unwrap();
#402	effect_num += 1;
#403	}
#404	}
#405	}
#406	}
#407	}
#408	if analysis.has_close_semantics {
#409	writeln!(s, "{}. Close account, return rent to signer", effect_num).unwrap();
#410	}
#411	if !analysis.has_token_program && !analysis.has_close_semantics {
#412	// Creation or state change
#413	if analysis.name.contains("init") {
#414	writeln!(s, "{}. Create account and initialize state", effect_num).unwrap();
#415	} else {
#416	writeln!(s, "{}. <!-- TODO: Describe effects -->", effect_num).unwrap();
#417	}
#418	}
#419	writeln!(s).unwrap();
#420
#421	// Postconditions
#422	writeln!(s, "Postconditions:").unwrap();
#423	if analysis.has_close_semantics {
#424	writeln!(s, "- Account MUST NOT exist (closed)").unwrap();
#425	}
#426	if analysis.name.contains("init") {
#427	for (arg_name, _) in &analysis.args {
#428	writeln!(s, "- State `{}` MUST equal the provided argument", arg_name).unwrap();
#429	}
#430	}
#431	writeln!(s, "- <!-- TODO: Add postconditions -->\n").unwrap();
#432	}
#433
#434	// §3 Formal Properties
#435	writeln!(s, "## 3. Formal Properties\n").unwrap();
#436
#437	// Access control
#438	if !signers_instructions.is_empty() {
#439	writeln!(s, "### 3.1 Access Control\n").unwrap();
#440	for analysis in &signers_instructions {
#441	writeln!(s, "{}_access_control: For all states `s` and signers `p`,",
#442	analysis.name).unwrap();
#443	writeln!(s, "if `{}Transition(s, p) ≠ none` then `p = s.{}`. ",
#444	analysis.name,
#445	analysis.has_one_relations.first()
#446	.map(\|(_, r)\| r.as_str())
#447	.unwrap_or("<!-- TODO: authority field -->")).unwrap();
#448	writeln!(s).unwrap();
#449	}
#450	}
#451
#452	// CPI correctness
#453	if !cpi_instructions.is_empty() {
#454	writeln!(s, "### 3.2 CPI Parameter Correctness\n").unwrap();
#455	for analysis in &cpi_instructions {
#456	writeln!(s, "{}_cpi_correct: For all contexts `ctx`,", analysis.name).unwrap();
#457	writeln!(s, "`{}_build_transfer_cpi(ctx)` MUST have correct `program`, `from`, `to`, `authority`, and `amount` fields matching the context. ",
#458	analysis.name).unwrap();
#459	writeln!(s).unwrap();
#460	}
#461	}
#462
#463	// State machine
#464	if !close_instructions.is_empty() {
#465	writeln!(s, "### 3.3 State Machine Safety\n").unwrap();
#466	for analysis in &close_instructions {
#467	writeln!(s, "{}_closes_account: For all states `s, s'`,", analysis.name).unwrap();
#468	writeln!(s, "if `{}Transition(s) = some s'` then `s'.lifecycle = closed`. ", analysis.name).unwrap();
#469	writeln!(s).unwrap();
#470	}
#471	}
#472
#473	// Arithmetic
#474	if !numeric_instructions.is_empty() {
#475	writeln!(s, "### 3.4 Arithmetic Safety\n").unwrap();
#476	writeln!(s, "arithmetic_bounds: All numeric parameters MUST satisfy `value ≤ MAX` after any computation. ").unwrap();
#477	writeln!(s).unwrap();
#478	}
#479
#480	// §4 Trust Boundary
#481	writeln!(s, "## 4. Trust Boundary\n").unwrap();
#482	writeln!(s, "The following are axiomatic (not verified):\n").unwrap();
#483	writeln!(s, "- SPL Token program: Transfer semantics are correct. We verify parameters passed, not the transfer itself.").unwrap();
#484	writeln!(s, "- Solana runtime: PDA derivation, account ownership enforcement, rent collection.").unwrap();
#485	writeln!(s, "- Anchor framework: Constraint enforcement (`has_one`, `signer`, account deserialization, close semantics).").unwrap();
#486	writeln!(s).unwrap();
#487
#488	// §5 Verification Results (empty table)
#489	writeln!(s, "## 5. Verification Results\n").unwrap();
#490	writeln!(s, "\| Property \| Status \| Proof \|").unwrap();
#491	writeln!(s, "\|---\|---\|---\|").unwrap();
#492	for analysis in analyses {
#493	if !analysis.signers.is_empty() {
#494	writeln!(s, "\| {}_access_control \| Open \| \|", analysis.name).unwrap();
#495	}
#496	if analysis.has_token_program {
#497	writeln!(s, "\| {}_cpi_correct \| Open \| \|", analysis.name).unwrap();
#498	}
#499	if analysis.has_close_semantics {
#500	writeln!(s, "\| {}_closes_account \| Open \| \|", analysis.name).unwrap();
#501	}
#502	}
#503	if analyses.iter().any(\|a\| a.has_numeric_args) {
#504	writeln!(s, "\| arithmetic_bounds \| Open \| \|").unwrap();
#505	}
#506	writeln!(s).unwrap();
#507
#508	s
#509	}
#510
#511	fn type_label(value: &serde_json::Value) -> String {
#512	match value {
#513	serde_json::Value::String(s) => s.clone(),
#514	other => other.to_string(),
#515	}
#516	}
#517
#518	fn snake_to_title(s: &str) -> String {
#519	s.split('_')
#520	.map(\|word\| {
#521	let mut chars = word.chars();
#522	match chars.next() {
#523	None => String::new(),
#524	Some(first) => first.to_uppercase().collect::<String>() + chars.as_str(),
#525	}
#526	})
#527	.collect::<Vec<_>>()
#528	.join(" ")
#529	}
#530

z6Mkq5mY3JWtxoxUobWcfNHm7AkRubgSWEZTkBVqZXJviFZ5/my-project-public