provable_contracts/lint/
rules.rs

1//! Lint rule catalog — every `pv lint` rule has an ID, default severity, and description.
2//!
3//! Rule ID format: `PV-<CATEGORY>-NNN`
4//! Categories: VAL (validation), AUD (audit), SCR (score), PRV (provability), TRD (trend)
5//!
6//! Spec: `docs/specifications/sub/lint.md` Section 12
7
8use serde::{Deserialize, Serialize};
9
10/// A lint rule definition.
11#[derive(Debug, Clone, Serialize)]
12pub struct LintRule {
13    pub id: &'static str,
14    pub category: RuleCategory,
15    pub default_severity: RuleSeverity,
16    pub description: &'static str,
17    /// Estimated remediation effort in minutes.
18    pub effort_minutes: u32,
19}
20
21/// Rule categories.
22#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
23#[serde(rename_all = "lowercase")]
24pub enum RuleCategory {
25    Validate,
26    Audit,
27    Score,
28    Provability,
29    Trend,
30    Suppression,
31    Enforcement,
32}
33
34/// Configurable severity levels per rule.
35#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize, PartialOrd, Ord)]
36#[serde(rename_all = "lowercase")]
37pub enum RuleSeverity {
38    Off,
39    Info,
40    Warning,
41    Error,
42}
43
44impl RuleSeverity {
45    pub fn from_str_opt(s: &str) -> Option<Self> {
46        match s {
47            "off" => Some(Self::Off),
48            "info" => Some(Self::Info),
49            "warning" | "warn" => Some(Self::Warning),
50            "error" => Some(Self::Error),
51            _ => None,
52        }
53    }
54
55    pub fn as_str(self) -> &'static str {
56        match self {
57            Self::Off => "off",
58            Self::Info => "info",
59            Self::Warning => "warning",
60            Self::Error => "error",
61        }
62    }
63
64    pub fn sarif_level(self) -> &'static str {
65        match self {
66            Self::Off => "none",
67            Self::Info => "note",
68            Self::Warning => "warning",
69            Self::Error => "error",
70        }
71    }
72}
73
74/// All lint rules in the catalog.
75pub static RULES: &[LintRule] = &[
76    // Validation rules (5 min each — fix YAML syntax)
77    LintRule {
78        id: "PV-VAL-001",
79        category: RuleCategory::Validate,
80        default_severity: RuleSeverity::Error,
81        description: "Schema validation error (parse failure or missing section)",
82        effort_minutes: 5,
83    },
84    LintRule {
85        id: "PV-VAL-002",
86        category: RuleCategory::Validate,
87        default_severity: RuleSeverity::Error,
88        description: "Missing metadata.version",
89        effort_minutes: 5,
90    },
91    LintRule {
92        id: "PV-VAL-003",
93        category: RuleCategory::Validate,
94        default_severity: RuleSeverity::Warning,
95        description: "Missing metadata.created",
96        effort_minutes: 5,
97    },
98    LintRule {
99        id: "PV-VAL-004",
100        category: RuleCategory::Validate,
101        default_severity: RuleSeverity::Error,
102        description: "Empty equation formula",
103        effort_minutes: 5,
104    },
105    LintRule {
106        id: "PV-VAL-005",
107        category: RuleCategory::Validate,
108        default_severity: RuleSeverity::Error,
109        description: "Empty proof obligation property",
110        effort_minutes: 5,
111    },
112    LintRule {
113        id: "PV-VAL-006",
114        category: RuleCategory::Validate,
115        default_severity: RuleSeverity::Warning,
116        description: "Duplicate formal predicate in proof obligations",
117        effort_minutes: 5,
118    },
119    // Audit rules (15 min each — add test/reference/domain)
120    LintRule {
121        id: "PV-AUD-001",
122        category: RuleCategory::Audit,
123        default_severity: RuleSeverity::Warning,
124        description: "Obligation without falsification test",
125        effort_minutes: 15,
126    },
127    LintRule {
128        id: "PV-AUD-002",
129        category: RuleCategory::Audit,
130        default_severity: RuleSeverity::Info,
131        description: "Missing paper reference",
132        effort_minutes: 15,
133    },
134    LintRule {
135        id: "PV-AUD-003",
136        category: RuleCategory::Audit,
137        default_severity: RuleSeverity::Warning,
138        description: "Obligation ID not referenced by any test",
139        effort_minutes: 15,
140    },
141    LintRule {
142        id: "PV-AUD-004",
143        category: RuleCategory::Audit,
144        default_severity: RuleSeverity::Warning,
145        description: "Equation without domain specification",
146        effort_minutes: 15,
147    },
148    LintRule {
149        id: "PV-AUD-005",
150        category: RuleCategory::Audit,
151        default_severity: RuleSeverity::Warning,
152        description: "Missing tolerance for numerical obligation",
153        effort_minutes: 15,
154    },
155    // Score rules (30 min each — improve score dimension)
156    LintRule {
157        id: "PV-SCR-001",
158        category: RuleCategory::Score,
159        default_severity: RuleSeverity::Error,
160        description: "Composite score below threshold",
161        effort_minutes: 30,
162    },
163    LintRule {
164        id: "PV-SCR-002",
165        category: RuleCategory::Score,
166        default_severity: RuleSeverity::Warning,
167        description: "Missing binding entry for equation",
168        effort_minutes: 30,
169    },
170    LintRule {
171        id: "PV-SCR-003",
172        category: RuleCategory::Score,
173        default_severity: RuleSeverity::Info,
174        description: "Kani coverage below 50%",
175        effort_minutes: 30,
176    },
177    LintRule {
178        id: "PV-SCR-004",
179        category: RuleCategory::Score,
180        default_severity: RuleSeverity::Info,
181        description: "Lean coverage at 0%",
182        effort_minutes: 30,
183    },
184    // Provability rules (60 min each — add Kani harness or falsification test)
185    LintRule {
186        id: "PV-PRV-001",
187        category: RuleCategory::Provability,
188        default_severity: RuleSeverity::Error,
189        description: "Kernel contract without Kani harnesses",
190        effort_minutes: 60,
191    },
192    LintRule {
193        id: "PV-PRV-002",
194        category: RuleCategory::Provability,
195        default_severity: RuleSeverity::Error,
196        description: "Kernel contract without falsification tests",
197        effort_minutes: 60,
198    },
199    LintRule {
200        id: "PV-PRV-003",
201        category: RuleCategory::Provability,
202        default_severity: RuleSeverity::Warning,
203        description: "Kani harness count < obligation count",
204        effort_minutes: 60,
205    },
206    LintRule {
207        id: "PV-PRV-004",
208        category: RuleCategory::Provability,
209        default_severity: RuleSeverity::Info,
210        description: "No Lean theorems (L5 not attempted)",
211        effort_minutes: 60,
212    },
213    // Trend rules (10 min each — review trend)
214    LintRule {
215        id: "PV-TRD-001",
216        category: RuleCategory::Trend,
217        default_severity: RuleSeverity::Warning,
218        description: "Mean score dropped >5% from 7-day rolling average",
219        effort_minutes: 10,
220    },
221    LintRule {
222        id: "PV-TRD-002",
223        category: RuleCategory::Trend,
224        default_severity: RuleSeverity::Info,
225        description: "Error count increased from previous snapshot",
226        effort_minutes: 10,
227    },
228    // Suppression rules (2 min each — remove stale suppression)
229    LintRule {
230        id: "PV-SUP-001",
231        category: RuleCategory::Suppression,
232        default_severity: RuleSeverity::Warning,
233        description: "Stale suppression — the finding no longer fires",
234        effort_minutes: 2,
235    },
236    // Enforcement rules (Section 17, Gaps 1 + 5)
237    LintRule {
238        id: "PV-ENF-001",
239        category: RuleCategory::Enforcement,
240        default_severity: RuleSeverity::Warning,
241        description: "Equation without preconditions",
242        effort_minutes: 20,
243    },
244    LintRule {
245        id: "PV-ENF-002",
246        category: RuleCategory::Enforcement,
247        default_severity: RuleSeverity::Warning,
248        description: "Equation without lean_theorem",
249        effort_minutes: 20,
250    },
251    LintRule {
252        id: "PV-LCK-001",
253        category: RuleCategory::Enforcement,
254        default_severity: RuleSeverity::Error,
255        description: "Contract regressed below locked verification level",
256        effort_minutes: 5,
257    },
258];
259
260/// Look up a rule by ID.
261pub fn find_rule(id: &str) -> Option<&'static LintRule> {
262    RULES.iter().find(|r| r.id == id)
263}
264
265/// Get all rules for a category.
266pub fn rules_for_category(cat: RuleCategory) -> Vec<&'static LintRule> {
267    RULES.iter().filter(|r| r.category == cat).collect()
268}
269
270#[cfg(test)]
271mod tests {
272    use super::*;
273
274    #[test]
275    fn rule_catalog_not_empty() {
276        assert!(!RULES.is_empty());
277        assert!(RULES.len() >= 21, "Expected 21+ rules, got {}", RULES.len());
278    }
279
280    #[test]
281    fn all_rule_ids_unique() {
282        let mut seen = std::collections::HashSet::new();
283        for rule in RULES {
284            assert!(seen.insert(rule.id), "Duplicate rule ID: {}", rule.id);
285        }
286    }
287
288    #[test]
289    fn find_rule_by_id() {
290        let rule = find_rule("PV-VAL-001").unwrap();
291        assert_eq!(rule.category, RuleCategory::Validate);
292        assert_eq!(rule.default_severity, RuleSeverity::Error);
293    }
294
295    #[test]
296    fn find_rule_missing() {
297        assert!(find_rule("PV-FAKE-999").is_none());
298    }
299
300    #[test]
301    fn rules_for_category_validate() {
302        let vals = rules_for_category(RuleCategory::Validate);
303        assert!(vals.len() >= 6);
304        assert!(vals.iter().all(|r| r.category == RuleCategory::Validate));
305    }
306
307    #[test]
308    fn severity_from_str() {
309        assert_eq!(
310            RuleSeverity::from_str_opt("error"),
311            Some(RuleSeverity::Error)
312        );
313        assert_eq!(
314            RuleSeverity::from_str_opt("warning"),
315            Some(RuleSeverity::Warning)
316        );
317        assert_eq!(
318            RuleSeverity::from_str_opt("warn"),
319            Some(RuleSeverity::Warning)
320        );
321        assert_eq!(RuleSeverity::from_str_opt("info"), Some(RuleSeverity::Info));
322        assert_eq!(RuleSeverity::from_str_opt("off"), Some(RuleSeverity::Off));
323        assert_eq!(RuleSeverity::from_str_opt("bogus"), None);
324    }
325
326    #[test]
327    fn severity_as_str_roundtrip() {
328        for sev in [
329            RuleSeverity::Off,
330            RuleSeverity::Info,
331            RuleSeverity::Warning,
332            RuleSeverity::Error,
333        ] {
334            let s = sev.as_str();
335            assert_eq!(RuleSeverity::from_str_opt(s), Some(sev));
336        }
337    }
338
339    #[test]
340    fn severity_sarif_level() {
341        assert_eq!(RuleSeverity::Error.sarif_level(), "error");
342        assert_eq!(RuleSeverity::Warning.sarif_level(), "warning");
343        assert_eq!(RuleSeverity::Info.sarif_level(), "note");
344        assert_eq!(RuleSeverity::Off.sarif_level(), "none");
345    }
346
347    #[test]
348    fn severity_ordering() {
349        assert!(RuleSeverity::Off < RuleSeverity::Info);
350        assert!(RuleSeverity::Info < RuleSeverity::Warning);
351        assert!(RuleSeverity::Warning < RuleSeverity::Error);
352    }
353
354    #[test]
355    fn rule_serializes() {
356        let json = serde_json::to_string(&RULES[0]).unwrap();
357        assert!(json.contains("PV-VAL-001"));
358        assert!(json.contains("validate"));
359    }
360}
provable_contracts/lint/rules.rs

provable_contracts/lint/
rules.rs
