use std::collections::BTreeSet;
use crate::schema::Contract;
#[derive(Debug, Clone)]
pub struct ContractDiff {
pub old_version: String,
pub new_version: String,
pub sections: Vec<SectionDiff>,
pub suggested_bump: SemverBump,
}
#[derive(Debug, Clone)]
pub struct SectionDiff {
pub section: String,
pub added: Vec<String>,
pub removed: Vec<String>,
pub changed: Vec<String>,
}
impl SectionDiff {
pub fn is_empty(&self) -> bool {
self.added.is_empty() && self.removed.is_empty() && self.changed.is_empty()
}
}
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum SemverBump {
None,
Patch,
Minor,
Major,
}
impl std::fmt::Display for SemverBump {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
match self {
Self::None => write!(f, "none"),
Self::Patch => write!(f, "patch"),
Self::Minor => write!(f, "minor"),
Self::Major => write!(f, "major"),
}
}
}
pub fn diff_contracts(old: &Contract, new: &Contract) -> ContractDiff {
let mut sections = Vec::new();
let mut max_bump = SemverBump::None;
let eq_diff = diff_keys(
"equations",
&old.equations.keys().cloned().collect(),
&new.equations.keys().cloned().collect(),
);
let eq_changed = diff_equation_changes(old, new);
let eq_section = SectionDiff {
section: "equations".to_string(),
added: eq_diff.0,
removed: eq_diff.1,
changed: eq_changed,
};
max_bump = bump_max(
max_bump,
section_bump(&eq_section, SemverBump::Major, SemverBump::Minor),
);
sections.push(eq_section);
let old_obs: BTreeSet<String> = old
.proof_obligations
.iter()
.map(|o| format!("{}:{}", o.obligation_type, o.property))
.collect();
let new_obs: BTreeSet<String> = new
.proof_obligations
.iter()
.map(|o| format!("{}:{}", o.obligation_type, o.property))
.collect();
let ob_diff = diff_sets("proof_obligations", &old_obs, &new_obs);
max_bump = bump_max(
max_bump,
section_bump(&ob_diff, SemverBump::Major, SemverBump::Minor),
);
sections.push(ob_diff);
let old_ft: BTreeSet<String> = old
.falsification_tests
.iter()
.map(|t| t.id.clone())
.collect();
let new_ft: BTreeSet<String> = new
.falsification_tests
.iter()
.map(|t| t.id.clone())
.collect();
let ft_diff = diff_sets("falsification_tests", &old_ft, &new_ft);
max_bump = bump_max(
max_bump,
section_bump(&ft_diff, SemverBump::Minor, SemverBump::Minor),
);
sections.push(ft_diff);
let old_kh: BTreeSet<String> = old.kani_harnesses.iter().map(|h| h.id.clone()).collect();
let new_kh: BTreeSet<String> = new.kani_harnesses.iter().map(|h| h.id.clone()).collect();
let kh_diff = diff_sets("kani_harnesses", &old_kh, &new_kh);
max_bump = bump_max(
max_bump,
section_bump(&kh_diff, SemverBump::Minor, SemverBump::Minor),
);
sections.push(kh_diff);
let old_enf: BTreeSet<String> = old.enforcement.keys().cloned().collect();
let new_enf: BTreeSet<String> = new.enforcement.keys().cloned().collect();
let enf_diff = diff_sets("enforcement", &old_enf, &new_enf);
max_bump = bump_max(
max_bump,
section_bump(&enf_diff, SemverBump::Minor, SemverBump::Patch),
);
sections.push(enf_diff);
if old.metadata.version != new.metadata.version {
max_bump = bump_max(max_bump, SemverBump::Patch);
}
ContractDiff {
old_version: old.metadata.version.clone(),
new_version: new.metadata.version.clone(),
sections,
suggested_bump: max_bump,
}
}
fn diff_keys(
_section: &str,
old_keys: &BTreeSet<String>,
new_keys: &BTreeSet<String>,
) -> (Vec<String>, Vec<String>) {
let added: Vec<String> = new_keys.difference(old_keys).cloned().collect();
let removed: Vec<String> = old_keys.difference(new_keys).cloned().collect();
(added, removed)
}
fn diff_sets(section: &str, old: &BTreeSet<String>, new: &BTreeSet<String>) -> SectionDiff {
let added: Vec<String> = new.difference(old).cloned().collect();
let removed: Vec<String> = old.difference(new).cloned().collect();
SectionDiff {
section: section.to_string(),
added,
removed,
changed: Vec::new(),
}
}
fn diff_equation_changes(old: &Contract, new: &Contract) -> Vec<String> {
let mut changed = Vec::new();
for (name, old_eq) in &old.equations {
if let Some(new_eq) = new.equations.get(name) {
if old_eq.formula != new_eq.formula {
changed.push(format!("{name}: formula changed"));
}
if old_eq.domain != new_eq.domain {
changed.push(format!("{name}: domain changed"));
}
if old_eq.codomain != new_eq.codomain {
changed.push(format!("{name}: codomain changed"));
}
if old_eq.invariants != new_eq.invariants {
changed.push(format!("{name}: invariants changed"));
}
}
}
changed
}
fn section_bump(section: &SectionDiff, on_break: SemverBump, on_add: SemverBump) -> SemverBump {
if !section.removed.is_empty() || !section.changed.is_empty() {
on_break
} else if !section.added.is_empty() {
on_add
} else {
SemverBump::None
}
}
fn bump_max(current: SemverBump, candidate: SemverBump) -> SemverBump {
let rank = |b: SemverBump| match b {
SemverBump::None => 0,
SemverBump::Patch => 1,
SemverBump::Minor => 2,
SemverBump::Major => 3,
};
if rank(candidate) > rank(current) {
candidate
} else {
current
}
}
pub fn is_identical(diff: &ContractDiff) -> bool {
diff.sections.iter().all(SectionDiff::is_empty) && diff.suggested_bump == SemverBump::None
}
#[cfg(test)]
mod tests {
include!("diff_tests.rs");
}