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

provable_contracts/lint/
rules.rs
