elicitation 0.11.1

//! Foundation Kani constructibility harness generator.
//!
//! Scans a crate source tree for `#[derive(Elicit)]` structs and enums and
//! emits a single `foundation.rs` file with one `#[kani::proof]` harness per
//! type, deduplicated by function name.
//!
//! Three harness shapes are emitted depending on the item kind:
//!
//! - **Enum with all unit variants** — direct construction via the first variant:
//!   ```ignore
//!   #[kani::proof]
//!   fn verify_{lower}_constructible() {
//!       let _: Ty = Ty::FirstVariant;
//!   }
//!   ```
//!
//! - **Type with `KaniCompose`** — uses `KaniCompose::kani_depth0()`:
//!   ```ignore
//!   #[cfg_attr(kani, ::kani::proof)]
//!   fn verify_{lower}_kani_compose() {
//!       let _: Ty = <Ty as ::elicitation::KaniCompose>::kani_depth0();
//!   }
//!   ```
//!
//! - **Struct or data-carrying enum without `KaniCompose`** — uses `kani::any()`
//!   (type must implement `kani::Arbitrary`):
//!   ```ignore
//!   #[cfg_attr(kani, ::kani::proof)]
//!   fn verify_{lower}_newtype_wrapper() {
//!       let _: Ty = kani::any();
//!   }
//!   ```

use quote::ToTokens;
use std::collections::HashSet;
use std::path::Path;
use syn::{File, Item};
use walkdir::WalkDir;

use super::find_crate_name;

// ─── Public types ─────────────────────────────────────────────────────────────

/// Describes a single `#[derive(Elicit)]` type discovered during scanning.
#[derive(Debug, Clone)]
pub struct ElicitType {
    /// The type name, e.g. `Board`.
    pub name: String,
    /// The harness shape to emit.
    pub shape: HarnessShape,
}

/// The shape of the Kani harness to emit for a given type.
#[derive(Debug, Clone)]
pub enum HarnessShape {
    /// Enum with all unit variants — use `Ty::FirstVariant`.
    Constructible {
        /// The first unit variant name.
        first_variant: String,
    },
    /// Type with `KaniCompose` — use `<Ty as KaniCompose>::kani_depth0()`.
    KaniCompose,
    /// Struct or data-carrying enum without `KaniCompose` — use `kani::any()`.
    NewtypeWrapper,
}

// ─── Public API ───────────────────────────────────────────────────────────────

/// Scan `root` for `#[derive(Elicit)]` items and return their descriptors.
///
/// Files that cannot be parsed are silently skipped.
#[tracing::instrument(skip(root), fields(root = %root.as_ref().display()))]
pub fn scan_elicit_types(root: impl AsRef<Path>) -> Vec<ElicitType> {
    let mut results: Vec<ElicitType> = Vec::new();
    let mut seen_names: HashSet<String> = HashSet::new();

    for entry in WalkDir::new(root.as_ref())
        .follow_links(false)
        .into_iter()
        .filter_map(|e| e.ok())
        .filter(|e| e.file_type().is_file() && e.path().extension().is_some_and(|ext| ext == "rs"))
    {
        let path = entry.into_path();
        let src = match std::fs::read_to_string(&path) {
            Ok(s) => s,
            Err(e) => {
                tracing::warn!(file = %path.display(), error = %e, "read failed");
                continue;
            }
        };
        let syntax: File = match syn::parse_str(&src) {
            Ok(f) => f,
            Err(e) => {
                tracing::debug!(file = %path.display(), error = %e, "parse failed, skipping");
                continue;
            }
        };

        for item in &syntax.items {
            if let Some(et) = extract_elicit_type(item)
                && seen_names.insert(et.name.clone())
            {
                results.push(et);
            }
        }
    }

    tracing::info!(count = results.len(), "elicit type scan complete");
    results
}

/// Generate the `foundation.rs` content for a set of `ElicitType`s.
///
/// `crate_root` is used to derive the `use {crate_name}::*` import.
#[tracing::instrument(skip(types, crate_root), fields(count = types.len()))]
pub fn generate_foundation_file(types: &[ElicitType], crate_root: impl AsRef<Path>) -> String {
    let crate_name = find_crate_name(crate_root.as_ref());

    let mut lines: Vec<String> = vec![
        "// AUTO-GENERATED by `elicitation generate foundation` — DO NOT EDIT".to_string(),
        "//".to_string(),
        "// Kani constructibility harnesses for all #[derive(Elicit)] types.".to_string(),
        "// Regenerate: elicitation generate foundation --crate-path <root>".to_string(),
        String::new(),
    ];

    // ── Import ───────────────────────────────────────────────────────────────
    if !types.is_empty() {
        let type_list: Vec<&str> = types.iter().map(|t| t.name.as_str()).collect();
        lines.push(format!("use {crate_name}::{{{}}};", type_list.join(", ")));
        lines.push(String::new());
    }

    // ── Harnesses ────────────────────────────────────────────────────────────
    let mut seen_fns: HashSet<String> = HashSet::new();
    for et in types {
        let fn_name = harness_fn_name(et);
        if !seen_fns.insert(fn_name.clone()) {
            tracing::debug!(fn_name, "skipping duplicate harness");
            continue;
        }
        lines.push(emit_harness(et, &fn_name));
    }

    lines.join("\n")
}

// ─── Internals ────────────────────────────────────────────────────────────────

/// Extract an `ElicitType` from a syn `Item`, or return `None`.
fn extract_elicit_type(item: &Item) -> Option<ElicitType> {
    match item {
        Item::Struct(s) if has_derive_elicit(&s.attrs) => {
            let shape = if has_cfg_attr_kani_compose(&s.attrs) || has_derive_kani_compose(&s.attrs)
            {
                HarnessShape::KaniCompose
            } else {
                HarnessShape::NewtypeWrapper
            };
            Some(ElicitType {
                name: s.ident.to_string(),
                shape,
            })
        }
        Item::Enum(e) if has_derive_elicit(&e.attrs) => {
            let first_unit = e
                .variants
                .iter()
                .find(|v| v.fields.is_empty())
                .map(|v| v.ident.to_string());
            match first_unit {
                Some(variant) if e.variants.iter().all(|v| v.fields.is_empty()) => {
                    Some(ElicitType {
                        name: e.ident.to_string(),
                        shape: HarnessShape::Constructible {
                            first_variant: variant,
                        },
                    })
                }
                _ => {
                    let shape = if has_cfg_attr_kani_compose(&e.attrs)
                        || has_derive_kani_compose(&e.attrs)
                    {
                        HarnessShape::KaniCompose
                    } else {
                        HarnessShape::NewtypeWrapper
                    };
                    Some(ElicitType {
                        name: e.ident.to_string(),
                        shape,
                    })
                }
            }
        }
        _ => None,
    }
}

/// Return `true` if the attribute list contains `#[derive(Elicit)]` (or
/// `#[derive(..., Elicit, ...)]` or `#[derive(..., some::crate::Elicit, ...)]`).
fn has_derive_elicit(attrs: &[syn::Attribute]) -> bool {
    attrs.iter().any(|a| {
        if !a.path().is_ident("derive") {
            return false;
        }
        a.parse_args_with(
            syn::punctuated::Punctuated::<syn::Path, syn::Token![,]>::parse_terminated,
        )
        .map(|paths| {
            paths
                .iter()
                .any(|p| p.segments.last().is_some_and(|seg| seg.ident == "Elicit"))
        })
        .unwrap_or(false)
    })
}

/// Return `true` if attrs contain `#[cfg_attr(kani, derive(... KaniCompose ...))]`.
///
/// Types with `KaniCompose` should use `kani_depth0()` rather than `kani::any()`,
/// since they may not implement `kani::Arbitrary` (e.g. types with `AtomicUsize`
/// fields or complex nested structures that cannot auto-derive `Arbitrary`).
fn has_cfg_attr_kani_compose(attrs: &[syn::Attribute]) -> bool {
    attrs.iter().any(|a| {
        if !a.path().is_ident("cfg_attr") {
            return false;
        }
        // Parse `cfg_attr(kani, derive(...))` — we only need to detect KaniCompose
        // anywhere in the token stream; a simple string search is sufficient.
        a.to_token_stream().to_string().contains("KaniCompose")
    })
}

/// Return `true` if attrs contain `#[derive(... KaniCompose ...)]` (plain, not cfg_attr).
///
/// Some types (e.g. VSM state enums) use a plain `#[derive(KaniCompose)]` because
/// the `KaniCompose` derive macro gates its generated code with `#[cfg(kani)]`
/// internally, so it is safe to place outside a `cfg_attr`.
fn has_derive_kani_compose(attrs: &[syn::Attribute]) -> bool {
    attrs.iter().any(|a| {
        if !a.path().is_ident("derive") {
            return false;
        }
        a.to_token_stream().to_string().contains("KaniCompose")
    })
}

/// Derive the harness function name for an `ElicitType`.
fn harness_fn_name(et: &ElicitType) -> String {
    let lower = to_snake(&et.name);
    match &et.shape {
        HarnessShape::Constructible { .. } => format!("verify_{lower}_constructible"),
        HarnessShape::KaniCompose => format!("verify_{lower}_kani_compose"),
        HarnessShape::NewtypeWrapper => format!("verify_{lower}_newtype_wrapper"),
    }
}

/// Emit one harness block as a string (without trailing newline).
fn emit_harness(et: &ElicitType, fn_name: &str) -> String {
    match &et.shape {
        HarnessShape::Constructible { first_variant } => {
            format!(
                "#[kani::proof]\nfn {fn_name}() {{\n    let _: {ty} = {ty}::{v};\n}}",
                ty = et.name,
                v = first_variant,
            )
        }
        HarnessShape::KaniCompose => {
            format!(
                "#[cfg_attr(kani, ::kani::proof)]\nfn {fn_name}() {{\n    let _: {ty} = <{ty} as ::elicitation::KaniCompose>::kani_depth0();\n}}",
                ty = et.name,
            )
        }
        HarnessShape::NewtypeWrapper => {
            format!(
                "#[cfg_attr(kani, ::kani::proof)]\nfn {fn_name}() {{\n    let _: {ty} = kani::any();\n}}",
                ty = et.name,
            )
        }
    }
}

/// Convert PascalCase to snake_case (mirrors the same fn in other generators).
fn to_snake(s: &str) -> String {
    let mut out = String::new();
    for (i, c) in s.chars().enumerate() {
        if c.is_uppercase() && i != 0 {
            out.push('_');
        }
        out.push(c.to_ascii_lowercase());
    }
    out
}