Skip to main content

provable_contracts/lint/
mod.rs

1//! Contract quality gate: validate + audit + score in one pass.
2//!
3//! Runs three sequential gates across all contracts in a directory:
4//! 1. **validate** — schema completeness (SCHEMA-001..013, PROVABILITY-001)
5//! 2. **audit** — traceability chain (paper→equation→obligation→test→proof)
6//! 3. **score** — 5-dimension quality score vs threshold
7//!
8//! Extended with SARIF output, rule catalog, config file, and findings.
9//! Spec: `docs/specifications/sub/lint.md`
10
11pub mod cache;
12mod composition_gate;
13pub mod config;
14pub mod diff;
15pub mod duplicate_stems;
16pub mod finding;
17mod gates;
18mod gates_extended;
19pub mod rules;
20pub mod sarif;
21mod strict_test_binding;
22pub mod trend;
23
24use std::collections::{HashMap, HashSet};
25use std::path::Path;
26use std::time::Instant;
27
28use serde::Serialize;
29
30use self::finding::LintFinding;
31use self::gates::{
32    load_binding, load_contracts, run_audit_gate, run_score_gate, run_validate_gate,
33};
34use self::gates_extended::{
35    check_stale_suppressions, run_enforce_gate, run_enforcement_level_gate,
36    run_reverse_coverage_gate, run_verify_gate,
37};
38use self::rules::RuleSeverity;
39
40/// Result of a single gate execution.
41#[derive(Debug, Clone, Serialize)]
42pub struct GateResult {
43    pub name: String,
44    pub passed: bool,
45    pub skipped: bool,
46    pub duration_ms: u64,
47    pub detail: GateDetail,
48    /// Structured payload for gates invented AFTER `GateDetail` was frozen.
49    ///
50    /// See [`GateExtra`] for why this second channel exists. Adding a field to a
51    /// struct is invisible to a `match` on `GateDetail`, which is the property
52    /// the 0.3.1 compatibility corpus depends on; adding a *variant* is not.
53    /// Serialised only when present, so existing JSON output is unchanged.
54    #[serde(default, skip_serializing_if = "Option::is_none")]
55    pub extra: Option<GateExtra>,
56}
57
58/// Gate-specific detail payload.
59///
60/// # This enum is FROZEN at the eight variants published in `provable-contracts`
61/// 0.3.1 — do not add a ninth
62///
63/// `GateDetail` is public, is not `#[non_exhaustive]`, and 0.3.1 shipped 28 example
64/// programs that `match` it exhaustively. Those programs are vendored verbatim under
65/// `crates/facades/provable-contracts/compat/0.3.1/`, sha256-verified against their
66/// published checksums by `scripts/check_facade_compat.sh` (row R6), and compiled in
67/// the `ci` job that the required `gate` check depends on. A ninth variant is
68/// `error[E0004]` in that corpus, and the corpus cannot be edited to accommodate it —
69/// being uneditable is the whole point of a compatibility contract. Marking the enum
70/// `#[non_exhaustive]` does not help either: it makes the *existing* exhaustive
71/// matches non-exhaustive, which is the same compile error for the same reason.
72///
73/// So the vocabulary is closed. A gate added after 0.3.1 picks the truest of these
74/// eight for `detail` and carries its own shape in [`GateResult::extra`], which is a
75/// type 0.3.1 never names and is therefore free to grow.
76#[derive(Debug, Clone, Serialize)]
77#[serde(tag = "type")]
78pub enum GateDetail {
79    #[serde(rename = "validate")]
80    Validate {
81        contracts: usize,
82        errors: usize,
83        warnings: usize,
84        error_messages: Vec<String>,
85    },
86    #[serde(rename = "audit")]
87    Audit {
88        contracts: usize,
89        findings: usize,
90        finding_messages: Vec<String>,
91    },
92    #[serde(rename = "score")]
93    Score {
94        contracts: usize,
95        min_score: f64,
96        mean_score: f64,
97        threshold: f64,
98        below_threshold: Vec<String>,
99    },
100    #[serde(rename = "verify")]
101    Verify {
102        total_refs: usize,
103        existing: usize,
104        missing: usize,
105    },
106    #[serde(rename = "enforce")]
107    Enforce {
108        equations_total: usize,
109        equations_with_pre: usize,
110        equations_with_post: usize,
111        equations_with_lean: usize,
112    },
113    #[serde(rename = "reverse_coverage")]
114    ReverseCoverage {
115        total_pub_fns: usize,
116        bound_fns: usize,
117        unbound_fns: usize,
118        coverage_pct: f64,
119        threshold_pct: f64,
120    },
121    #[serde(rename = "composition")]
122    Composition {
123        edges_checked: usize,
124        edges_satisfied: usize,
125        edges_broken: usize,
126    },
127    #[serde(rename = "skipped")]
128    Skipped { reason: String },
129}
130
131/// Out-of-band structured detail for gates that post-date the frozen [`GateDetail`]
132/// vocabulary.
133///
134/// This type did not exist in `provable-contracts` 0.3.1, so no 0.3.1 program names
135/// it and none can `match` it. That is what makes it extensible where `GateDetail` is
136/// not, and it is `#[non_exhaustive]` from birth so the *next* post-0.3.1 gate does
137/// not have to repeat this exercise.
138#[derive(Debug, Clone, Serialize)]
139#[serde(tag = "type")]
140#[non_exhaustive]
141pub enum GateExtra {
142    /// PV-DUP-001: contract stems claimed by several files with divergent content.
143    #[serde(rename = "duplicate_stems")]
144    DuplicateStems {
145        /// Total ambiguous stems found in the tree.
146        divergent: usize,
147        /// How many of those are recorded in the ratchet baseline.
148        baselined: usize,
149        /// Ambiguous stems NOT in the baseline — these fail the gate.
150        unbaselined: Vec<String>,
151        /// Baseline entries that no longer diverge — these fail the gate too.
152        stale: Vec<String>,
153        /// Every ambiguous stem, with its variant count and paths, for the report.
154        divergent_stems: Vec<String>,
155    },
156}
157
158/// Overall lint report.
159#[derive(Debug, Clone, Serialize)]
160pub struct LintReport {
161    pub passed: bool,
162    pub gates: Vec<GateResult>,
163    pub total_duration_ms: u64,
164    #[serde(skip_serializing_if = "Vec::is_empty")]
165    pub findings: Vec<LintFinding>,
166    #[serde(skip)]
167    pub cache_stats: cache::CacheStats,
168    /// Per-contract processing times: `(contract_stem, duration_ms)`.
169    #[serde(default, skip_serializing_if = "Vec::is_empty")]
170    pub contract_timings: Vec<(String, u64)>,
171}
172
173/// Configuration for `pv lint`.
174pub struct LintConfig<'a> {
175    pub contract_dir: &'a Path,
176    pub binding_path: Option<&'a Path>,
177    pub min_score: f64,
178    pub severity_filter: Option<RuleSeverity>,
179    pub severity_overrides: HashMap<String, RuleSeverity>,
180    pub suppressed_findings: Vec<String>,
181    pub suppressed_rules: Vec<String>,
182    pub suppressed_files: Vec<String>,
183    pub strict: bool,
184    pub no_cache: bool,
185    pub cache_stats: bool,
186    /// Optional crate directory for reverse coverage gate (Gate 7).
187    pub crate_dir: Option<&'a Path>,
188    /// Minimum enforcement level for Gate 6 (from `--min-level`).
189    pub min_level: Option<crate::schema::EnforcementLevel>,
190    /// Enable Gate 9 (strict test-binding, PV-VER-002). Issue #1510.
191    pub strict_test_binding: bool,
192}
193
194impl<'a> LintConfig<'a> {
195    /// Create a basic config (backward compatible).
196    pub fn new(contract_dir: &'a Path, binding_path: Option<&'a Path>, min_score: f64) -> Self {
197        Self {
198            contract_dir,
199            binding_path,
200            min_score,
201            severity_filter: None,
202            severity_overrides: HashMap::new(),
203            suppressed_findings: Vec::new(),
204            suppressed_rules: Vec::new(),
205            suppressed_files: Vec::new(),
206            strict: false,
207            no_cache: false,
208            cache_stats: false,
209            crate_dir: None,
210            min_level: None,
211            strict_test_binding: false,
212        }
213    }
214}
215
216/// Run all lint gates across a contract directory.
217#[allow(clippy::too_many_lines)]
218pub fn run_lint(config: &LintConfig) -> LintReport {
219    let overall_start = Instant::now();
220    let mut gates = Vec::with_capacity(3);
221    let mut all_findings = Vec::new();
222    let mut stats = cache::CacheStats::default();
223    let mut contract_timings: Vec<(String, u64)> = Vec::new();
224
225    let cache_root = if config.no_cache {
226        None
227    } else {
228        Some(cache::cache_dir(config.contract_dir))
229    };
230
231    let (contracts, parse_errors) = load_contracts(config.contract_dir);
232    let binding = load_binding(config.binding_path);
233
234    // Gate 1: validate
235    let (validate_result, mut validate_findings) = run_validate_gate(&contracts, &parse_errors);
236    let validation_passed = validate_result.passed;
237    gates.push(validate_result);
238
239    // Gate 2: audit (skip if validation failed)
240    if validation_passed {
241        let (audit_result, mut audit_findings) = run_audit_gate(&contracts);
242        gates.push(audit_result);
243        all_findings.append(&mut audit_findings);
244    } else {
245        gates.push(skipped_gate("audit", "validation failed"));
246    }
247
248    // Gate 3: score (skip if validation failed)
249    if validation_passed {
250        let (score_result, mut score_findings) =
251            run_score_gate(&contracts, binding.as_ref(), config.min_score);
252        gates.push(score_result);
253        all_findings.append(&mut score_findings);
254    } else {
255        gates.push(skipped_gate("score", "validation failed"));
256    }
257
258    // Gate 4: verify (source code fulfillment)
259    if validation_passed {
260        let project_root = config.contract_dir.parent().unwrap_or(config.contract_dir);
261        let (verify_result, mut verify_findings) = run_verify_gate(&contracts, project_root);
262        gates.push(verify_result);
263        all_findings.append(&mut verify_findings);
264    } else {
265        gates.push(skipped_gate("verify", "validation failed"));
266    }
267
268    // Gate 5: enforce (equations must have preconditions/postconditions)
269    if validation_passed {
270        let (enforce_result, mut enforce_findings) = run_enforce_gate(&contracts);
271        gates.push(enforce_result);
272        all_findings.append(&mut enforce_findings);
273    } else {
274        gates.push(skipped_gate("enforce", "validation failed"));
275    }
276
277    // Gate 6: enforcement level (Section 17, Gap 1 + Gap 5 level lock)
278    if validation_passed {
279        let min_level = config
280            .min_level
281            .unwrap_or(crate::schema::EnforcementLevel::Standard);
282        let (level_result, mut level_findings) = run_enforcement_level_gate(&contracts, min_level);
283        gates.push(level_result);
284        all_findings.append(&mut level_findings);
285    } else {
286        gates.push(skipped_gate("enforcement-level", "validation failed"));
287    }
288
289    // Gate 7: reverse coverage (optional — skip if no binding or crate dir)
290    if validation_passed {
291        if let (Some(bp), Some(cd)) = (config.binding_path, config.crate_dir) {
292            let (rev_result, mut rev_findings) = run_reverse_coverage_gate(bp, cd);
293            gates.push(rev_result);
294            all_findings.append(&mut rev_findings);
295        } else {
296            gates.push(skipped_gate(
297                "reverse-coverage",
298                "no --binding or --crate-dir provided",
299            ));
300        }
301    } else {
302        gates.push(skipped_gate("reverse-coverage", "validation failed"));
303    }
304
305    // Gate 8: duplicate stems (PV-DUP-001). Must run BEFORE composition — it tells
306    // the composition gate which stems are unresolvable, which is the difference
307    // between a defined verdict and one decided by `read_dir` order.
308    let duplicates = duplicate_stems::scan_duplicate_stems(config.contract_dir);
309    let ambiguous = duplicate_stems::ambiguous_stems(&duplicates);
310    if validation_passed {
311        let project_root = config.contract_dir.parent().unwrap_or(config.contract_dir);
312        let baseline = duplicate_stems::read_baseline(project_root);
313        let (dup_result, mut dup_findings) =
314            duplicate_stems::run_duplicate_stem_gate(&duplicates, &baseline);
315        gates.push(dup_result);
316        all_findings.append(&mut dup_findings);
317    } else {
318        gates.push(skipped_gate("duplicate-stems", "validation failed"));
319    }
320
321    // Gate 9: composition (assumes/guarantees chain verification)
322    if validation_passed {
323        let (comp_result, mut comp_findings) =
324            composition_gate::run_composition_gate(&contracts, &ambiguous);
325        gates.push(comp_result);
326        all_findings.append(&mut comp_findings);
327    } else {
328        gates.push(skipped_gate("composition", "validation failed"));
329    }
330
331    // Gate 9: strict test-binding (Issue #1510, opt-in via --strict-test-binding)
332    if config.strict_test_binding {
333        if validation_passed {
334            let project_root = config.contract_dir.parent().unwrap_or(config.contract_dir);
335            let (binding_result, mut binding_findings) =
336                strict_test_binding::run_strict_test_binding_gate(
337                    &contracts,
338                    project_root,
339                    config.strict,
340                );
341            gates.push(binding_result);
342            all_findings.append(&mut binding_findings);
343        } else {
344            gates.push(skipped_gate("strict-test-binding", "validation failed"));
345        }
346    }
347
348    all_findings.append(&mut validate_findings);
349
350    // Per-contract timing: measure how long each contract's findings take to process
351    if validation_passed {
352        for (stem, contract) in &contracts {
353            let ct_start = Instant::now();
354            // Validate
355            let _ = crate::schema::validate_contract(contract);
356            // Audit
357            let _ = crate::audit::audit_contract(contract);
358            // Score
359            let _ = crate::scoring::score_contract(contract, binding.as_ref(), stem);
360            let ct_ms = u64::try_from(ct_start.elapsed().as_micros() / 1000).unwrap_or(0);
361            contract_timings.push((format!("{stem}.yaml"), ct_ms));
362        }
363        // Sort by duration descending
364        contract_timings.sort_by_key(|b| std::cmp::Reverse(b.1));
365    }
366
367    // Stale suppression detection (PV-SUP-001, Section 17 Gap 2)
368    let mut stale_findings = check_stale_suppressions(
369        &all_findings,
370        &config.suppressed_rules,
371        &config.suppressed_findings,
372    );
373    all_findings.append(&mut stale_findings);
374
375    // Issue lifecycle: mark each finding as new or pre-existing
376    mark_new_findings(&mut all_findings, config.contract_dir);
377
378    // Cache: store findings per-contract for future runs
379    if let Some(ref root) = cache_root {
380        let rule_cfg = format!("{:?}{:?}", config.severity_overrides, config.strict);
381        for (stem, _) in &contracts {
382            stats.total += 1;
383            let yaml_path = config.contract_dir.join(format!("{stem}.yaml"));
384            let yaml_content = std::fs::read_to_string(&yaml_path).unwrap_or_default();
385            let hash = cache::content_hash(&yaml_content, &rule_cfg);
386            if cache::cache_get(root, &hash).is_some() {
387                stats.hits += 1;
388            } else {
389                stats.misses += 1;
390                let contract_findings: Vec<_> = all_findings
391                    .iter()
392                    .filter(|f| f.contract_stem.as_deref() == Some(stem.as_str()))
393                    .cloned()
394                    .collect();
395                let _ = cache::cache_put(root, &hash, &contract_findings);
396            }
397        }
398    }
399
400    // Apply suppressions, severity overrides, strict mode, and severity filter
401    apply_suppressions(&mut all_findings, config);
402    apply_severity_overrides(&mut all_findings, config);
403    if let Some(min_sev) = config.severity_filter {
404        all_findings.retain(|f| f.severity >= min_sev);
405    }
406
407    let passed = gates.iter().all(|g| g.passed || g.skipped);
408
409    LintReport {
410        passed,
411        gates,
412        total_duration_ms: u64::try_from(overall_start.elapsed().as_millis()).unwrap_or(u64::MAX),
413        findings: all_findings,
414        cache_stats: stats,
415        contract_timings,
416    }
417}
418
419fn skipped_gate(name: &str, reason: &str) -> GateResult {
420    GateResult {
421        name: name.into(),
422        passed: false,
423        skipped: true,
424        duration_ms: 0,
425        detail: GateDetail::Skipped {
426            reason: reason.into(),
427        },
428        extra: None,
429    }
430}
431
432fn apply_suppressions(findings: &mut [LintFinding], config: &LintConfig) {
433    for f in findings.iter_mut() {
434        if config.suppressed_rules.iter().any(|r| r == &f.rule_id) {
435            f.suppressed = true;
436            f.suppression_reason = Some("Suppressed by --suppress-rule".into());
437        }
438        if let Some(ref stem) = f.contract_stem {
439            if config.suppressed_findings.iter().any(|s| s == stem) {
440                f.suppressed = true;
441                f.suppression_reason = Some("Suppressed by --suppress".into());
442            }
443        }
444        if config.suppressed_files.iter().any(|p| f.file.contains(p)) {
445            f.suppressed = true;
446            f.suppression_reason = Some("Suppressed by --suppress-file".into());
447        }
448    }
449}
450
451/// Resolve the `.pv/` state directory relative to the contract directory's parent.
452fn pv_state_dir(contract_dir: &Path) -> std::path::PathBuf {
453    contract_dir.parent().unwrap_or(contract_dir).join(".pv")
454}
455
456/// Load previous fingerprints, compare with current findings, mark new ones,
457/// and persist the current fingerprint set for the next run.
458fn mark_new_findings(findings: &mut [LintFinding], contract_dir: &Path) {
459    let state_dir = pv_state_dir(contract_dir);
460    let previous_path = state_dir.join("lint-previous.json");
461
462    // Load previous fingerprints (empty set if file missing or unreadable)
463    let previous: HashSet<String> = std::fs::read_to_string(&previous_path)
464        .ok()
465        .and_then(|s| serde_json::from_str(&s).ok())
466        .unwrap_or_default();
467
468    // Compute current fingerprints and mark new findings
469    let mut current = HashSet::new();
470    for f in findings.iter_mut() {
471        let fp = f.fingerprint();
472        if !previous.contains(&fp) {
473            f.is_new = true;
474        }
475        current.insert(fp);
476    }
477
478    // Persist current fingerprints for the next run
479    if let Err(e) = std::fs::create_dir_all(&state_dir) {
480        eprintln!("pv lint: cannot create {}: {e}", state_dir.display());
481        return;
482    }
483    if let Ok(json) = serde_json::to_string(&current) {
484        let _ = std::fs::write(&previous_path, json);
485    }
486}
487
488fn apply_severity_overrides(findings: &mut [LintFinding], config: &LintConfig) {
489    for f in findings.iter_mut() {
490        if let Some(&sev) = config.severity_overrides.get(&f.rule_id) {
491            f.severity = sev;
492        }
493    }
494    if config.strict {
495        for f in findings.iter_mut() {
496            if f.severity == RuleSeverity::Warning {
497                f.severity = RuleSeverity::Error;
498            }
499        }
500    }
501}
502
503#[cfg(test)]
504#[path = "mod_tests.rs"]
505mod tests;