blvm-spec-lock 0.1.8

//! Enrich spec-locked functions with contracts from the Orange Paper.

use super::verify::{Contract, ContractType, FunctionToVerify};
use crate::parser::condition;
use crate::parser::orange_paper::{ContractType as SpecContractType, SpecParser};
use std::path::PathBuf;

fn find_function_in_section_or_parents<'a>(
    parser: &'a SpecParser,
    section: &str,
    name: Option<&str>,
) -> Option<&'a crate::parser::orange_paper::FunctionSpec> {
    let mut s = section;
    loop {
        if let Some(f) = parser.find_function(s, name) {
            return Some(f);
        }
        if let Some(dot) = s.rfind('.') {
            s = &s[..dot];
        } else {
            break;
        }
    }
    None
}

/// Convert Rust snake_case to spec PascalCase (e.g. get_block_subsidy -> GetBlockSubsidy)
fn rust_to_spec_name(rust_name: &str) -> String {
    rust_name
        .split('_')
        .map(|s| {
            let mut c = s.chars();
            match c.next() {
                None => String::new(),
                Some(f) => f.to_uppercase().chain(c).collect(),
            }
        })
        .collect()
}

/// Enrich discovered functions with contracts extracted from the Orange Paper.
/// Accepts one or more spec paths; when multiple, sections are merged (duplicate section IDs error).
pub fn enrich_functions_with_spec(
    functions: &mut [FunctionToVerify],
    spec_paths: &[PathBuf],
) -> Result<usize, String> {
    let parser = SpecParser::from_paths(spec_paths)?;

    let mut enriched_count = 0;

    for func in functions.iter_mut() {
        let section = match &func.section {
            Some(s) => s,
            None => continue,
        };

        let spec_name = rust_to_spec_name(&func.function_name);

        let spec_func = parser
            .find_function(section, Some(&spec_name))
            .or_else(|| parser.find_function_anywhere(&spec_name).map(|(f, _)| f))
            .or_else(|| parser.find_function(section, None))
            .or_else(|| find_function_in_section_or_parents(&parser, section, None));
        let spec_func = spec_func.and_then(|f| {
            if f.contracts.is_empty() {
                parser.find_function(section, Some("*"))
            } else {
                Some(f)
            }
        });

        if let Some(spec_func) = spec_func {
            if spec_func.contracts.is_empty() {
                continue;
            }

            func.contracts.clear();

            let mut added_any = false;
            for spec_contract in &spec_func.contracts {
                let contract_type = match spec_contract.contract_type {
                    SpecContractType::Requires => ContractType::Requires,
                    SpecContractType::Ensures
                    | SpecContractType::Property
                    | SpecContractType::EdgeCase => ContractType::Ensures,
                };

                let condition = spec_contract.condition.trim().to_string();
                if condition.is_empty() {
                    continue;
                }

                let parseable = condition::extract_parseable_condition(&condition);
                let expr = parseable
                    .as_ref()
                    .and_then(|s| syn::parse_str::<syn::Expr>(s).ok());

                if expr.is_none() {
                    continue;
                }

                let contract = Contract {
                    contract_type,
                    condition: condition.clone(),
                    expr,
                };

                if !func.contracts.iter().any(|c| c.condition == condition) {
                    func.contracts.push(contract);
                    enriched_count += 1;
                    added_any = true;
                }
            }

            if !added_any && !spec_func.contracts.is_empty() {
                if let Ok(expr) = syn::parse_str::<syn::Expr>("true") {
                    func.contracts.push(Contract {
                        contract_type: ContractType::Ensures,
                        condition: "true".to_string(),
                        expr: Some(expr),
                    });
                    enriched_count += 1;
                }
            }
        }

        // Fallback: spec has no parseable contracts for this section (e.g. complex math only).
        // Add default ensures(true) so verification doesn't fail with "no contracts".
        // Keeps Orange Paper focused on math; tooling handles the rest.
        if func.contracts.is_empty() && func.section.is_some() {
            if let Ok(expr) = syn::parse_str::<syn::Expr>("true") {
                func.contracts.push(Contract {
                    contract_type: ContractType::Ensures,
                    condition: "true".to_string(),
                    expr: Some(expr),
                });
                enriched_count += 1;
            }
        }
    }

    Ok(enriched_count)
}