agent-spec 1.1.0

Intent compiler for AI agent coding: human intent compiles through requirement IR into verifiable task contracts, mechanically verified against the code
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108

//! Derived liveness (§7). Never stored; computed from current spec verdicts.

use crate::spec_core::{Verdict, VerificationSummary};
use crate::spec_knowledge::model::{Liveness, LivenessDeclared};

/// Roll a single spec's verification summary into one representative verdict:
/// Fail if anything failed; Pass only if every scenario passed; otherwise a
/// not-yet-proven verdict (Skip stands in for skip/uncertain/pending/empty).
pub fn spec_rollup(summary: &VerificationSummary) -> Verdict {
    if summary.failed > 0 {
        Verdict::Fail
    } else if summary.total == 0
        || summary.skipped > 0
        || summary.uncertain > 0
        || summary.pending_review > 0
    {
        Verdict::Skip
    } else {
        Verdict::Pass
    }
}

/// Precedence ladder (§7), total and mutually exclusive:
/// 1. declared `n/a`            -> Na
/// 2. any satisfying spec Fail  -> Violated
/// 3. none, or any not-Pass     -> Unproven
/// 4. all Pass                  -> Honored
pub fn decision_liveness(declared: LivenessDeclared, spec_verdicts: &[Verdict]) -> Liveness {
    if declared == LivenessDeclared::Na {
        return Liveness::Na;
    }
    if spec_verdicts.contains(&Verdict::Fail) {
        return Liveness::Violated;
    }
    if spec_verdicts.is_empty() || spec_verdicts.iter().any(|v| *v != Verdict::Pass) {
        return Liveness::Unproven;
    }
    Liveness::Honored
}

#[cfg(test)]
#[allow(clippy::unwrap_used)]
mod tests {
    use super::*;

    fn summary(total: usize, passed: usize, failed: usize, skipped: usize) -> VerificationSummary {
        VerificationSummary {
            total,
            passed,
            failed,
            skipped,
            uncertain: 0,
            pending_review: 0,
        }
    }

    #[test]
    fn test_spec_rollup_fail_dominates() {
        assert_eq!(spec_rollup(&summary(3, 2, 1, 0)), Verdict::Fail);
    }

    #[test]
    fn test_spec_rollup_all_pass() {
        assert_eq!(spec_rollup(&summary(2, 2, 0, 0)), Verdict::Pass);
    }

    #[test]
    fn test_spec_rollup_skip_is_not_pass() {
        assert_eq!(spec_rollup(&summary(2, 1, 0, 1)), Verdict::Skip);
        assert_eq!(spec_rollup(&summary(0, 0, 0, 0)), Verdict::Skip);
    }

    #[test]
    fn test_liveness_na_short_circuits() {
        assert_eq!(
            decision_liveness(LivenessDeclared::Na, &[Verdict::Fail]),
            Liveness::Na
        );
    }

    #[test]
    fn test_liveness_violated_on_any_fail() {
        assert_eq!(
            decision_liveness(LivenessDeclared::Auto, &[Verdict::Pass, Verdict::Fail]),
            Liveness::Violated
        );
    }

    #[test]
    fn test_liveness_unproven_when_empty_or_not_all_pass() {
        assert_eq!(
            decision_liveness(LivenessDeclared::Auto, &[]),
            Liveness::Unproven
        );
        assert_eq!(
            decision_liveness(LivenessDeclared::Auto, &[Verdict::Pass, Verdict::Skip]),
            Liveness::Unproven
        );
    }

    #[test]
    fn test_liveness_honored_when_all_pass() {
        assert_eq!(
            decision_liveness(LivenessDeclared::Auto, &[Verdict::Pass, Verdict::Pass]),
            Liveness::Honored
        );
    }
}