use std::collections::{BTreeSet, HashMap};
use crate::binding::{normalize_contract_id, BindingRegistry, ImplStatus};
use crate::schema::{Contract, LeanStatus};
use super::score_contract;
use super::types::{CodebaseScore, Grade, ScoringGap};
#[allow(clippy::cast_precision_loss)]
pub fn score_codebase(
contracts: &[(String, &Contract)],
binding: &BindingRegistry,
) -> CodebaseScore {
score_codebase_with_pagerank(contracts, binding, None)
}
#[allow(clippy::cast_precision_loss, clippy::implicit_hasher)]
pub fn score_codebase_with_pagerank(
contracts: &[(String, &Contract)],
binding: &BindingRegistry,
pagerank: Option<&HashMap<String, f64>>,
) -> CodebaseScore {
score_codebase_full(contracts, binding, pagerank, None)
}
#[allow(clippy::cast_precision_loss, clippy::implicit_hasher)]
pub fn score_codebase_full(
contracts: &[(String, &Contract)],
binding: &BindingRegistry,
pagerank: Option<&HashMap<String, f64>>,
drift_override: Option<f64>,
) -> CodebaseScore {
let bound_stems: BTreeSet<_> = binding
.bindings
.iter()
.map(|b| b.contract.as_str())
.collect();
let unique_declared: BTreeSet<_> = binding
.bindings
.iter()
.map(|b| normalize_contract_id(&b.contract))
.collect();
let declared_count = unique_declared.len();
let contract_coverage = if declared_count == 0 {
0.0
} else {
let resolved = unique_declared
.iter()
.filter(|stem| {
contracts
.iter()
.any(|(s, _)| normalize_contract_id(s) == **stem)
})
.count();
resolved as f64 / declared_count as f64
};
let total_bindings = binding.bindings.len();
let implemented_bindings: f64 = binding
.bindings
.iter()
.map(|b| match b.status {
ImplStatus::Implemented => 1.0,
ImplStatus::Partial => 0.5,
ImplStatus::NotImplemented | ImplStatus::Pending => 0.0,
})
.sum();
let binding_completeness = if total_bindings == 0 {
0.0
} else {
implemented_bindings / total_bindings as f64
};
let critical_path_coverage = if binding.critical_path.is_empty() {
binding_completeness } else {
let covered = binding
.critical_path
.iter()
.filter(|cp| {
binding.bindings.iter().any(|b| {
b.function
.as_deref()
.is_some_and(|f| f.contains(cp.as_str()))
})
})
.count();
#[allow(clippy::cast_precision_loss)]
let ratio = covered as f64 / binding.critical_path.len() as f64;
ratio
};
let bound_scores: Vec<f64> = contracts
.iter()
.filter(|(stem, _)| bound_stems.contains(stem.as_str()))
.map(|(stem, c)| score_contract(c, Some(binding), stem).composite)
.collect();
let mean_contract_score = if bound_scores.is_empty() {
0.0
} else {
bound_scores.iter().sum::<f64>() / bound_scores.len() as f64
};
let proof_depth_dist = compute_proof_depth(contracts, &bound_stems);
let drift = drift_override.unwrap_or(1.0);
let composite = contract_coverage * 0.25
+ critical_path_coverage * 0.20
+ mean_contract_score * 0.20
+ proof_depth_dist * 0.15
+ drift * 0.20;
let top_gaps = compute_gaps(contracts, binding, &bound_stems, pagerank);
CodebaseScore {
path: "codebase".to_string(),
contract_coverage,
binding_completeness: critical_path_coverage,
mean_contract_score,
proof_depth_dist,
drift,
reverse_coverage: 0.0,
mutation_testing: 1.0,
ci_pipeline_depth: 1.0,
proof_freshness: 1.0,
defect_patterns: 1.0,
composite,
grade: Grade::from_score(composite),
top_gaps,
}
}
#[allow(clippy::cast_precision_loss)]
fn compute_proof_depth(contracts: &[(String, &Contract)], bound_stems: &BTreeSet<&str>) -> f64 {
let mut total_obligations = 0usize;
let mut weighted_sum = 0.0;
for (stem, contract) in contracts {
if !bound_stems.contains(stem.as_str()) {
continue;
}
for ob in &contract.proof_obligations {
total_obligations += 1;
weighted_sum += 0.1; if !contract.falsification_tests.is_empty() {
weighted_sum += 0.3; }
if !contract.kani_harnesses.is_empty() {
weighted_sum += 0.4; }
if ob
.lean
.as_ref()
.is_some_and(|l| l.status == LeanStatus::Proved)
{
weighted_sum += 0.2; }
}
}
if total_obligations == 0 {
return 0.0;
}
(weighted_sum / total_obligations as f64).min(1.0)
}
#[allow(clippy::cast_precision_loss)]
fn compute_gaps(
contracts: &[(String, &Contract)],
binding: &BindingRegistry,
bound_stems: &BTreeSet<&str>,
pagerank: Option<&HashMap<String, f64>>,
) -> Vec<ScoringGap> {
let mut gaps = Vec::new();
let rev_dep_counts = compute_reverse_dep_counts(contracts);
for (stem, contract) in contracts {
if !bound_stems.contains(stem.as_str()) {
continue;
}
let ob_count = contract.proof_obligations.len();
let kani_count = contract.kani_harnesses.len();
let ft_count = contract.falsification_tests.len();
let fanout = dependency_fanout(stem, pagerank, &rev_dep_counts);
if ob_count > 0 && kani_count < ob_count {
let coverage = kani_count as f64 / ob_count as f64;
gaps.push(ScoringGap {
contract: stem.clone(),
dimension: "kani_coverage".into(),
current: coverage,
target: 1.0,
impact: (1.0 - coverage) * fanout,
action: "Write #[kani::proof] harnesses".into(),
});
}
if ob_count > 0 && ft_count < ob_count {
let coverage = ft_count as f64 / ob_count as f64;
gaps.push(ScoringGap {
contract: stem.clone(),
dimension: "falsification_coverage".into(),
current: coverage,
target: 1.0,
impact: (1.0 - coverage) * fanout,
action: "Write probar property tests".into(),
});
}
let partial_count = binding
.bindings_for(stem)
.iter()
.filter(|b| b.status == ImplStatus::Partial)
.count();
if partial_count > 0 {
gaps.push(ScoringGap {
contract: stem.clone(),
dimension: "binding_partial".into(),
current: 0.5,
target: 1.0,
impact: 0.5 * fanout,
action: "Complete partial implementations".into(),
});
}
let unimpl_count = binding
.bindings_for(stem)
.iter()
.filter(|b| b.status == ImplStatus::NotImplemented)
.count();
if unimpl_count > 0 {
gaps.push(ScoringGap {
contract: stem.clone(),
dimension: "binding_coverage".into(),
current: 0.0,
target: 1.0,
impact: 1.0 * fanout,
action: "Implement bound equations".into(),
});
}
}
gaps.sort_by(|a, b| {
b.impact
.partial_cmp(&a.impact)
.unwrap_or(std::cmp::Ordering::Equal)
});
gaps.truncate(10);
gaps
}
#[allow(clippy::cast_precision_loss)]
fn dependency_fanout(
stem: &str,
pagerank: Option<&HashMap<String, f64>>,
rev_dep_counts: &HashMap<&str, usize>,
) -> f64 {
if let Some(pr) = pagerank {
if let Some(&score) = pr.get(stem) {
let max_pr = pr.values().copied().fold(f64::NEG_INFINITY, f64::max);
let min_pr = pr.values().copied().fold(f64::INFINITY, f64::min);
let range = max_pr - min_pr;
if range > 1e-12 {
return 1.0 + 9.0 * (score - min_pr) / range;
}
}
}
(rev_dep_counts.get(stem).copied().unwrap_or(0) + 1) as f64
}
fn compute_reverse_dep_counts<'a>(contracts: &'a [(String, &Contract)]) -> HashMap<&'a str, usize> {
let mut counts: HashMap<&str, usize> = HashMap::new();
for (_, contract) in contracts {
for dep in &contract.metadata.depends_on {
for (stem, _) in contracts {
if stem == dep || stem.strip_suffix(".yaml").is_some_and(|s| s == dep) {
*counts.entry(stem.as_str()).or_default() += 1;
}
}
}
}
counts
}
#[cfg(test)]
#[path = "codebase_tests.rs"]
mod tests;