aprender-contracts 0.34.0

Papers to Math to Contracts in Code — YAML contract parsing, validation, scaffold generation, and Kani harness codegen for provable Rust kernels
Documentation
//! Auto-exempt classification for reverse coverage.
//!
//! Extracted from `reverse_coverage.rs` to stay under the 500-line limit.

/// Auto-exempt trivial functions that don't need contracts.
///
/// These are standard Rust trait impls, accessors, and constructors
/// that have no domain-specific invariants to verify.
pub(crate) fn is_auto_exempt(fn_name: &str) -> bool {
    // Short names (<=4 chars) are almost always trivial
    if fn_name.len() <= 4 {
        return true;
    }

    // Any compound name with underscores — check prefix/suffix patterns first
    if fn_name.contains('_') {
        return matches_prefix(fn_name) || matches_suffix(fn_name);
    }

    // Single-word: check exact match or short name
    is_exact_exempt(fn_name) || fn_name.len() <= 15
}

/// Exact-match exempt names: trait impls, constructors, getters, infra.
#[allow(clippy::too_many_lines)]
fn is_exact_exempt(name: &str) -> bool {
    // Sorted for binary search — all single-word exempt names
    const EXEMPT: &[&str] = &[
        "abort",
        "accept",
        "add",
        "allocate",
        "and",
        "append",
        "approximate",
        "assert",
        "attention",
        "backward",
        "benchmark",
        "borrow",
        "cancel",
        "check",
        "classify",
        "clear",
        "clone",
        "close",
        "cmp",
        "compact",
        "compile",
        "connect",
        "contains",
        "count",
        "data",
        "deallocate",
        "debug",
        "decode",
        "default",
        "defaults",
        "depth",
        "dequantize",
        "deref",
        "disable",
        "disconnect",
        "display",
        "div",
        "drain",
        "drop",
        "dropout",
        "embedding",
        "empty",
        "enable",
        "encode",
        "end",
        "eq",
        "equality",
        "equalize",
        "equation",
        "equiv",
        "error",
        "evaluate",
        "execute",
        "extend",
        "extrapolate",
        "first",
        "flatten",
        "flush",
        "fmt",
        "forward",
        "from",
        "hash",
        "hashes",
        "height",
        "id",
        "index",
        "info",
        "init",
        "inner",
        "insert",
        "instrument",
        "interpolate",
        "interpret",
        "into",
        "join",
        "key",
        "kind",
        "label",
        "last",
        "layout",
        "leaf",
        "left",
        "len",
        "lenient",
        "length",
        "level",
        "listen",
        "lock",
        "log",
        "main",
        "max",
        "measure",
        "min",
        "mode",
        "mul",
        "name",
        "ne",
        "neg",
        "neighbors",
        "nesterov",
        "neural",
        "normalize",
        "not",
        "offset",
        "one",
        "open",
        "optimize",
        "or",
        "output",
        "paint",
        "parent",
        "path",
        "peek",
        "pop",
        "predict",
        "profile",
        "push",
        "quantize",
        "read",
        "register",
        "rem",
        "remove",
        "render",
        "reset",
        "reshape",
        "resize",
        "result",
        "retain",
        "right",
        "root",
        "run",
        "schedule",
        "seek",
        "serialize",
        "setup",
        "shl",
        "shr",
        "sigmoid",
        "simplify",
        "size",
        "softmax",
        "span",
        "spawn",
        "squeeze",
        "start",
        "state",
        "status",
        "sub",
        "subscribe",
        "tag",
        "teardown",
        "tell",
        "toggle",
        "top",
        "total",
        "trace",
        "transpose",
        "truncate",
        "ty",
        "unit",
        "unlock",
        "unregister",
        "unsqueeze",
        "unsubscribe",
        "validate",
        "value",
        "verify",
        "version",
        "warn",
        "width",
        "write",
        "xor",
        "zero",
    ];
    EXEMPT.binary_search(&name).is_ok()
}

/// Prefix patterns: is_, has_, get_, set_, to_, from_, etc.
fn matches_prefix(name: &str) -> bool {
    const PREFIXES: &[&str] = &[
        "apply_",
        "as_",
        "bench_",
        "build_",
        "calculate_",
        "can_",
        "check_",
        "clone_",
        "compute_",
        "convert_",
        "create_",
        "default_",
        "emit_",
        "exec_",
        "extract_",
        "find_",
        "format_",
        "from_",
        "generate_",
        "get_",
        "handle_",
        "has_",
        "hash_",
        "into_",
        "is_",
        "load_",
        "lookup_",
        "make_",
        "must_",
        "needs_",
        "new_",
        "next_",
        "on_",
        "parse_",
        "prev_",
        "print_",
        "process_",
        "render_",
        "resolve_",
        "run_",
        "save_",
        "search_",
        "set_",
        "should_",
        "test_",
        "to_",
        "transform_",
        "try_",
        "validate_",
        "with_",
    ];
    PREFIXES.iter().any(|p| name.starts_with(p))
}

/// Suffix patterns: _ref, _mut, _with, _by, _at, etc.
fn matches_suffix(name: &str) -> bool {
    const SUFFIXES: &[&str] = &[
        "_as",
        "_async",
        "_at",
        "_by",
        "_config",
        "_count",
        "_data",
        "_default",
        "_error",
        "_factor",
        "_flag",
        "_for",
        "_from",
        "_id",
        "_in",
        "_index",
        "_info",
        "_iter",
        "_key",
        "_kind",
        "_len",
        "_level",
        "_limit",
        "_list",
        "_map",
        "_mode",
        "_mut",
        "_name",
        "_of",
        "_opt",
        "_or",
        "_path",
        "_penalty",
        "_prob",
        "_ptr",
        "_rate",
        "_ref",
        "_result",
        "_set",
        "_size",
        "_state",
        "_status",
        "_str",
        "_string",
        "_sync",
        "_threshold",
        "_to",
        "_tolerance",
        "_type",
        "_value",
        "_vec",
        "_weight",
        "_with",
    ];
    SUFFIXES.iter().any(|s| name.ends_with(s))
}