use std::collections::{BTreeMap, BTreeSet};
use proofborne_core::{
AssuranceLevel, ClaimScope, CriterionEvaluation, CriterionState, ProofGraph, ProofTermination,
RunOutcome, SCHEMA_VERSION, TaskContract,
};
use serde::{Deserialize, Serialize};
use uuid::Uuid;
#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)]
#[serde(rename_all = "camelCase")]
pub struct VerificationReport {
pub schema_version: String,
pub contract_id: Uuid,
pub valid: bool,
pub claim_scope: ClaimScope,
#[serde(skip_serializing_if = "Option::is_none")]
pub assurance_level: Option<AssuranceLevel>,
#[serde(skip_serializing_if = "Option::is_none")]
pub outcome: Option<RunOutcome>,
#[serde(default)]
pub criteria: Vec<CriterionEvaluation>,
#[serde(default)]
pub issues: Vec<VerificationIssue>,
}
impl VerificationReport {
pub fn proves_task(&self) -> bool {
self.valid
&& self.claim_scope == ClaimScope::Task
&& self.outcome == Some(RunOutcome::Verified)
}
pub fn is_verified(&self) -> bool {
self.valid
&& matches!(
self.outcome,
Some(RunOutcome::Verified | RunOutcome::VerifiedWithWaivers)
)
}
}
#[derive(Debug, Clone, Copy, Serialize, Deserialize, PartialEq, Eq, PartialOrd, Ord)]
#[serde(rename_all = "snake_case")]
pub enum VerificationSeverity {
Warning,
Error,
}
#[derive(Debug, Clone, Copy, Serialize, Deserialize, PartialEq, Eq, PartialOrd, Ord)]
#[serde(rename_all = "snake_case")]
pub enum VerificationIssueCode {
RuntimeClaimNotTaskCompletion,
NoMachineCheckableTaskEvidence,
UnsupportedSchema,
InvalidContract,
ContractMismatch,
EvidenceKeyMismatch,
UnknownEvidenceLink,
UnknownCriterionLink,
DuplicateLink,
TimestampOrder,
IncompleteAttempt,
EmptyIdentity,
IncompleteStateBinding,
DuplicateSupersession,
UnknownSupersession,
SelfSupersession,
SupersessionNotLater,
SupersessionWithoutCommonCriterion,
CriterionStateMismatch,
CriterionEvidenceMismatch,
IncompleteDecision,
EvaluationFailed,
}
#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)]
#[serde(rename_all = "camelCase")]
pub struct VerificationIssue {
pub code: VerificationIssueCode,
pub severity: VerificationSeverity,
pub message: String,
#[serde(skip_serializing_if = "Option::is_none")]
pub criterion_id: Option<String>,
#[serde(skip_serializing_if = "Option::is_none")]
pub evidence_id: Option<Uuid>,
}
pub fn verify(contract: &TaskContract, proof: &ProofGraph) -> VerificationReport {
let mut issues = Vec::new();
validate_versions(contract, proof, &mut issues);
validate_contract(contract, &mut issues);
validate_graph(contract, proof, &mut issues);
if contract.claim_scope == ClaimScope::Runtime {
push_warning(
&mut issues,
VerificationIssueCode::RuntimeClaimNotTaskCompletion,
"runtime-scoped evidence cannot produce a verified task outcome".to_owned(),
None,
None,
);
}
let mut reduced_contract = contract.clone();
let evaluation = match proof.evaluate_detailed(&mut reduced_contract) {
Ok(evaluation) => {
validate_persisted_derivation(contract, &reduced_contract, &mut issues);
if contract.claim_scope == ClaimScope::Task
&& evaluation.outcome != RunOutcome::VerifiedWithWaivers
&& !has_machine_checkable_task_evidence(contract, proof, &evaluation.criteria)
{
push_warning(
&mut issues,
VerificationIssueCode::NoMachineCheckableTaskEvidence,
"no required criterion has qualifying tool, process, or git evidence"
.to_owned(),
None,
None,
);
}
Some(evaluation)
}
Err(error) => {
push_issue(
&mut issues,
VerificationIssueCode::EvaluationFailed,
format!("deterministic proof reduction failed: {error}"),
None,
None,
);
None
}
};
issues.sort_by(|left, right| {
(
left.severity,
left.code,
&left.criterion_id,
left.evidence_id,
&left.message,
)
.cmp(&(
right.severity,
right.code,
&right.criterion_id,
right.evidence_id,
&right.message,
))
});
let valid = !issues
.iter()
.any(|issue| issue.severity == VerificationSeverity::Error);
VerificationReport {
schema_version: SCHEMA_VERSION.to_owned(),
contract_id: contract.id,
valid,
claim_scope: contract.claim_scope,
assurance_level: evaluation
.as_ref()
.map(|evaluation| evaluation.assurance_level),
outcome: evaluation.as_ref().map(|evaluation| evaluation.outcome),
criteria: evaluation
.map(|evaluation| evaluation.criteria)
.unwrap_or_default(),
issues,
}
}
fn has_machine_checkable_task_evidence(
contract: &TaskContract,
proof: &ProofGraph,
evaluations: &[CriterionEvaluation],
) -> bool {
contract
.criteria
.iter()
.filter(|criterion| criterion.required && criterion.state == CriterionState::Passed)
.filter_map(|criterion| {
evaluations
.iter()
.find(|evaluation| evaluation.criterion_id == criterion.id)
})
.flat_map(|evaluation| evaluation.qualifying_evidence_ids.iter())
.filter_map(|id| proof.evidence.get(id))
.any(|evidence| {
matches!(
evidence.kind,
proofborne_core::EvidenceKind::Tool
| proofborne_core::EvidenceKind::Process
| proofborne_core::EvidenceKind::Git
)
})
}
fn validate_versions(
contract: &TaskContract,
proof: &ProofGraph,
issues: &mut Vec<VerificationIssue>,
) {
if contract.schema_version != SCHEMA_VERSION {
push_issue(
issues,
VerificationIssueCode::UnsupportedSchema,
format!(
"contract schema {} is not supported; expected {SCHEMA_VERSION}",
contract.schema_version
),
None,
None,
);
}
if proof.schema_version != SCHEMA_VERSION {
push_issue(
issues,
VerificationIssueCode::UnsupportedSchema,
format!(
"proof schema {} is not supported; expected {SCHEMA_VERSION}",
proof.schema_version
),
None,
None,
);
}
}
fn validate_contract(contract: &TaskContract, issues: &mut Vec<VerificationIssue>) {
if contract.id.is_nil() {
push_issue(
issues,
VerificationIssueCode::ContractMismatch,
"contract identifier must not be nil".to_owned(),
None,
None,
);
}
if let Err(error) = contract.validate() {
push_issue(
issues,
VerificationIssueCode::InvalidContract,
error.to_string(),
None,
None,
);
}
if !contract.confirmed {
push_issue(
issues,
VerificationIssueCode::IncompleteDecision,
"finalized proof requires a confirmed task contract".to_owned(),
None,
None,
);
}
for criterion in &contract.criteria {
match (criterion.state, criterion.waiver.as_ref()) {
(CriterionState::Waived, None) => push_issue(
issues,
VerificationIssueCode::IncompleteDecision,
"waived criterion has no waiver metadata".to_owned(),
Some(criterion.id.clone()),
None,
),
(CriterionState::Waived, Some(waiver))
if waiver.actor.trim().is_empty() || waiver.reason.trim().is_empty() =>
{
push_issue(
issues,
VerificationIssueCode::IncompleteDecision,
"waiver actor and reason must not be empty".to_owned(),
Some(criterion.id.clone()),
None,
);
}
(
CriterionState::Pending | CriterionState::Passed | CriterionState::Failed,
Some(_),
) => {
push_issue(
issues,
VerificationIssueCode::IncompleteDecision,
"non-waived criterion contains waiver metadata".to_owned(),
Some(criterion.id.clone()),
None,
);
}
_ => {}
}
}
}
fn validate_graph(
contract: &TaskContract,
proof: &ProofGraph,
issues: &mut Vec<VerificationIssue>,
) {
if proof.contract_id != contract.id || proof.contract_id.is_nil() {
push_issue(
issues,
VerificationIssueCode::ContractMismatch,
"proof graph and contract identifiers do not agree".to_owned(),
None,
None,
);
}
if proof.final_state_binding.is_some() && proof.final_workspace_generation.is_none() {
push_issue(
issues,
VerificationIssueCode::IncompleteStateBinding,
"final state binding requires a final workspace generation".to_owned(),
None,
None,
);
}
if proof
.final_state_binding
.as_ref()
.is_some_and(|binding| binding.trim().is_empty())
{
push_issue(
issues,
VerificationIssueCode::IncompleteStateBinding,
"final state binding must not be empty".to_owned(),
None,
None,
);
}
if let Some(termination) = &proof.termination {
let reason = match termination {
ProofTermination::Blocked { reason } | ProofTermination::Cancelled { reason } => reason,
};
if reason.trim().is_empty() {
push_issue(
issues,
VerificationIssueCode::IncompleteDecision,
"proof termination reason must not be empty".to_owned(),
None,
None,
);
}
}
let criterion_ids: BTreeSet<_> = contract
.criteria
.iter()
.map(|criterion| criterion.id.as_str())
.collect();
let mut evidence_criteria: BTreeMap<Uuid, BTreeSet<&str>> = BTreeMap::new();
let mut seen_links = BTreeSet::new();
for link in &proof.links {
if !proof.evidence.contains_key(&link.evidence_id) {
push_issue(
issues,
VerificationIssueCode::UnknownEvidenceLink,
"proof link references missing evidence".to_owned(),
Some(link.criterion_id.clone()),
Some(link.evidence_id),
);
}
if !criterion_ids.contains(link.criterion_id.as_str()) {
push_issue(
issues,
VerificationIssueCode::UnknownCriterionLink,
"proof link references an unknown criterion".to_owned(),
Some(link.criterion_id.clone()),
Some(link.evidence_id),
);
}
if !seen_links.insert((link.evidence_id, link.criterion_id.as_str())) {
push_issue(
issues,
VerificationIssueCode::DuplicateLink,
"evidence-to-criterion link occurs more than once".to_owned(),
Some(link.criterion_id.clone()),
Some(link.evidence_id),
);
}
evidence_criteria
.entry(link.evidence_id)
.or_default()
.insert(link.criterion_id.as_str());
}
for (key, evidence) in &proof.evidence {
if *key != evidence.id {
push_issue(
issues,
VerificationIssueCode::EvidenceKeyMismatch,
format!(
"evidence map key {key} does not match embedded id {}",
evidence.id
),
None,
Some(*key),
);
}
if evidence.producer.trim().is_empty()
|| evidence.summary.trim().is_empty()
|| evidence
.action_id
.as_ref()
.is_some_and(|action| action.trim().is_empty())
{
push_issue(
issues,
VerificationIssueCode::EmptyIdentity,
"evidence producer, summary, and present action id must not be empty".to_owned(),
None,
Some(*key),
);
}
if evidence.completed_at < evidence.started_at {
push_issue(
issues,
VerificationIssueCode::TimestampOrder,
"evidence completed before it started".to_owned(),
None,
Some(*key),
);
}
if evidence.attempt_id.is_some() != evidence.attempt_sequence.is_some() {
push_issue(
issues,
VerificationIssueCode::IncompleteAttempt,
"attemptId and attemptSequence must be recorded together".to_owned(),
None,
Some(*key),
);
}
if evidence.state_binding.is_some() && evidence.workspace_generation.is_none() {
push_issue(
issues,
VerificationIssueCode::IncompleteStateBinding,
"evidence state binding requires a workspace generation".to_owned(),
None,
Some(*key),
);
}
if evidence
.state_binding
.as_ref()
.is_some_and(|binding| binding.trim().is_empty())
{
push_issue(
issues,
VerificationIssueCode::IncompleteStateBinding,
"evidence state binding must not be empty".to_owned(),
None,
Some(*key),
);
}
let mut seen_supersessions = BTreeSet::new();
for predecessor_id in &evidence.supersedes {
if !seen_supersessions.insert(*predecessor_id) {
push_issue(
issues,
VerificationIssueCode::DuplicateSupersession,
"superseded evidence identifier occurs more than once".to_owned(),
None,
Some(*key),
);
}
if predecessor_id == key || predecessor_id == &evidence.id {
push_issue(
issues,
VerificationIssueCode::SelfSupersession,
"evidence cannot supersede itself".to_owned(),
None,
Some(*key),
);
continue;
}
let Some(predecessor) = proof.evidence.get(predecessor_id) else {
push_issue(
issues,
VerificationIssueCode::UnknownSupersession,
format!("superseded evidence {predecessor_id} is not present"),
None,
Some(*key),
);
continue;
};
if !is_strictly_later(evidence, predecessor) {
push_issue(
issues,
VerificationIssueCode::SupersessionNotLater,
"supersession requires distinct attempts and a greater attempt sequence"
.to_owned(),
None,
Some(*key),
);
}
let successor_criteria = evidence_criteria.get(key);
let predecessor_criteria = evidence_criteria.get(predecessor_id);
let shares_criterion =
successor_criteria
.zip(predecessor_criteria)
.is_some_and(|(left, right)| {
left.iter().any(|criterion| right.contains(criterion))
});
if !shares_criterion {
push_issue(
issues,
VerificationIssueCode::SupersessionWithoutCommonCriterion,
"superseding evidence and predecessor share no linked criterion".to_owned(),
None,
Some(*key),
);
}
}
}
}
fn is_strictly_later(
successor: &proofborne_core::Evidence,
predecessor: &proofborne_core::Evidence,
) -> bool {
matches!(
(
successor.attempt_id,
successor.attempt_sequence,
predecessor.attempt_id,
predecessor.attempt_sequence,
),
(
Some(successor_id),
Some(successor_sequence),
Some(predecessor_id),
Some(predecessor_sequence),
) if successor_id != predecessor_id && successor_sequence > predecessor_sequence
)
}
fn validate_persisted_derivation(
original: &TaskContract,
reduced: &TaskContract,
issues: &mut Vec<VerificationIssue>,
) {
for (original_criterion, reduced_criterion) in original.criteria.iter().zip(&reduced.criteria) {
if original_criterion.state != reduced_criterion.state {
push_issue(
issues,
VerificationIssueCode::CriterionStateMismatch,
format!(
"persisted state {:?} recomputes to {:?}",
original_criterion.state, reduced_criterion.state
),
Some(original_criterion.id.clone()),
None,
);
}
let original_ids: BTreeSet<_> = original_criterion.evidence_ids.iter().copied().collect();
let reduced_ids: BTreeSet<_> = reduced_criterion.evidence_ids.iter().copied().collect();
if original_ids != reduced_ids {
push_issue(
issues,
VerificationIssueCode::CriterionEvidenceMismatch,
"persisted evidenceIds differ from deterministic graph links".to_owned(),
Some(original_criterion.id.clone()),
None,
);
}
}
}
fn push_issue(
issues: &mut Vec<VerificationIssue>,
code: VerificationIssueCode,
message: String,
criterion_id: Option<String>,
evidence_id: Option<Uuid>,
) {
issues.push(VerificationIssue {
code,
severity: VerificationSeverity::Error,
message,
criterion_id,
evidence_id,
});
}
fn push_warning(
issues: &mut Vec<VerificationIssue>,
code: VerificationIssueCode,
message: String,
criterion_id: Option<String>,
evidence_id: Option<Uuid>,
) {
issues.push(VerificationIssue {
code,
severity: VerificationSeverity::Warning,
message,
criterion_id,
evidence_id,
});
}
#[cfg(test)]
mod tests {
use chrono::Duration;
use proofborne_core::{Criterion, Evidence, EvidenceFreshness, EvidenceKind};
use serde_json::to_value;
use super::*;
fn finalized_task() -> (TaskContract, ProofGraph, Uuid) {
let mut criterion = Criterion::required("tests", "tests pass");
criterion.evidence_requirement.allowed_producers =
["proofborne.verify".to_owned()].into_iter().collect();
criterion.evidence_requirement.freshness = EvidenceFreshness::FinalWorkspaceGeneration;
let mut contract = TaskContract::new("prove the test", vec![criterion]);
contract.confirmed = true;
let mut proof = ProofGraph::new(contract.id);
proof.bind_final_workspace(1, None);
let evidence = Evidence::observed(
EvidenceKind::Process,
"proofborne.verify",
"test passed",
None,
None,
Some(0),
true,
)
.bound_to_workspace(1, None);
let evidence_id = proof.record(evidence);
proof.link(&contract, evidence_id, "tests", None).unwrap();
proof.evaluate(&mut contract).unwrap();
(contract, proof, evidence_id)
}
#[test]
fn valid_task_proof_returns_structured_report() {
let (contract, proof, evidence_id) = finalized_task();
let report = verify(&contract, &proof);
assert!(report.valid);
assert!(report.proves_task());
assert_eq!(report.claim_scope, ClaimScope::Task);
assert_eq!(report.outcome, Some(RunOutcome::Verified));
assert_eq!(report.assurance_level, Some(AssuranceLevel::Observed));
assert_eq!(
report.criteria[0].qualifying_evidence_ids,
vec![evidence_id]
);
assert!(report.issues.is_empty());
}
#[test]
fn former_false_completion_path_is_runtime_only() {
let mut contract = TaskContract::automatic("model merely stopped");
let mut proof = ProofGraph::new(contract.id);
let evidence = Evidence::observed(
EvidenceKind::Runtime,
"proofborne.runtime",
"terminal turn",
None,
None,
Some(0),
true,
);
let id = proof.record(evidence);
proof
.link(&contract, id, "runtime_completed", None)
.unwrap();
proof.evaluate(&mut contract).unwrap();
let report = verify(&contract, &proof);
assert!(report.valid);
assert!(!report.is_verified());
assert!(!report.proves_task());
assert_eq!(report.claim_scope, ClaimScope::Runtime);
assert_eq!(report.outcome, Some(RunOutcome::Blocked));
assert!(report.issues.iter().any(|issue| {
issue.code == VerificationIssueCode::RuntimeClaimNotTaskCompletion
&& issue.severity == VerificationSeverity::Warning
}));
}
#[test]
fn relabelled_auto_contract_is_invalid() {
let mut contract = TaskContract::automatic("model merely stopped");
contract.claim_scope = ClaimScope::Task;
let proof = ProofGraph::new(contract.id);
let report = verify(&contract, &proof);
assert!(!report.valid);
assert!(!report.proves_task());
assert!(report.issues.iter().any(|issue| {
issue.code == VerificationIssueCode::InvalidContract
|| issue.code == VerificationIssueCode::EvaluationFailed
}));
}
#[test]
fn unknown_link_and_stale_persisted_state_are_rejected() {
let (mut contract, mut proof, _) = finalized_task();
contract.criteria[0].state = CriterionState::Pending;
proof.links.push(proofborne_core::EvidenceLink {
evidence_id: Uuid::now_v7(),
criterion_id: "tests".to_owned(),
rationale: None,
});
let report = verify(&contract, &proof);
assert!(!report.valid);
assert!(
report
.issues
.iter()
.any(|issue| { issue.code == VerificationIssueCode::UnknownEvidenceLink })
);
assert!(
report
.issues
.iter()
.any(|issue| { issue.code == VerificationIssueCode::CriterionStateMismatch })
);
}
#[test]
fn invalid_supersession_and_timestamp_are_rejected() {
let (mut contract, mut proof, first_id) = finalized_task();
let attempt_id = Uuid::now_v7();
let first = proof.evidence.get_mut(&first_id).unwrap();
first.attempt_id = Some(attempt_id);
first.attempt_sequence = Some(2);
let mut successor = Evidence::observed(
EvidenceKind::Process,
"proofborne.verify",
"older result",
None,
None,
Some(0),
true,
)
.with_attempt(attempt_id, 1)
.superseding([first_id]);
successor.completed_at = successor.started_at - Duration::seconds(1);
let successor_id = proof.record(successor);
proof.link(&contract, successor_id, "tests", None).unwrap();
proof.evaluate(&mut contract).unwrap();
let report = verify(&contract, &proof);
assert!(!report.valid);
assert!(
report
.issues
.iter()
.any(|issue| { issue.code == VerificationIssueCode::SupersessionNotLater })
);
assert!(
report
.issues
.iter()
.any(|issue| issue.code == VerificationIssueCode::TimestampOrder)
);
}
#[test]
fn report_serialization_is_camel_case_and_deterministic() {
let (contract, proof, _) = finalized_task();
let first = to_value(verify(&contract, &proof)).unwrap();
let second = to_value(verify(&contract, &proof)).unwrap();
assert_eq!(first, second);
assert!(first.get("schemaVersion").is_some());
assert!(first.get("claimScope").is_some());
assert!(first.get("assuranceLevel").is_some());
}
}