pmat 3.29.0

PMAT - Zero-config AI context generation and code quality toolkit (CLI, MCP)
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
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146

// Proof annotation factory methods for RustBorrowChecker
// Included by rust_borrow_checker.rs - no `use` imports or `#!` attributes

impl RustBorrowChecker {
    /// Canonical seed for an annotation's id: the site plus the claim.
    ///
    /// DETERMINISM: see `crate::models::unified_ast::derive_annotation_id`.
    /// Every factory below used `Uuid::new_v4()`, so the same annotation about
    /// the same unchanged line got a brand new `annotationId` on every run.
    fn annotation_seed(&self, location: &Location, kind: &str) -> String {
        format!(
            "{}|{}-{}|{}|pmat-{}|{}",
            location.file_path.display(),
            location.span.start.0,
            location.span.end.0,
            kind,
            self.rustc_channel,
            self.rustc_version,
        )
    }

    /// Create memory safety annotation
    fn memory_safety_annotation(&self, location: &Location) -> ProofAnnotation {
        ProofAnnotation {
            annotation_id: crate::models::unified_ast::derive_annotation_id(
                &self.annotation_seed(location, "MemorySafety/BorrowChecker"),
            ),
            property_proven: PropertyType::MemorySafety,
            specification_id: None,
            method: VerificationMethod::BorrowChecker,
            // "pmat-syn-static-analysis", not a compiler that never ran.
            tool_name: format!("pmat-{}", self.rustc_channel),
            tool_version: self.rustc_version.clone(),
            confidence_level: ConfidenceLevel::High,
            assumptions: vec![
                "Safe Rust subset".to_string(),
                "No compiler bugs".to_string(),
            ],
            evidence_type: EvidenceType::ImplicitTypeSystemGuarantee,
            evidence_location: None,
            date_verified: chrono::Utc::now(),
        }
    }

    /// Create thread safety annotation
    fn create_thread_safety_annotation(&self, location: &Location) -> ProofAnnotation {
        ProofAnnotation {
            annotation_id: crate::models::unified_ast::derive_annotation_id(
                &self.annotation_seed(location, "ThreadSafety/BorrowChecker"),
            ),
            property_proven: PropertyType::ThreadSafety,
            specification_id: None,
            method: VerificationMethod::BorrowChecker,
            // "pmat-syn-static-analysis", not a compiler that never ran.
            tool_name: format!("pmat-{}", self.rustc_channel),
            tool_version: self.rustc_version.clone(),
            confidence_level: ConfidenceLevel::High,
            assumptions: vec![
                "Send + Sync bounds satisfied".to_string(),
                "No interior mutability without synchronization".to_string(),
            ],
            evidence_type: EvidenceType::ImplicitTypeSystemGuarantee,
            evidence_location: None,
            date_verified: chrono::Utc::now(),
        }
    }

    /// Create const fn termination annotation
    fn const_fn_termination(&self, location: &Location) -> ProofAnnotation {
        ProofAnnotation {
            annotation_id: crate::models::unified_ast::derive_annotation_id(
                &self.annotation_seed(location, "Termination/ConstFn"),
            ),
            property_proven: PropertyType::Termination,
            specification_id: None,
            method: VerificationMethod::BorrowChecker,
            // "pmat-syn-static-analysis", not a compiler that never ran.
            tool_name: format!("pmat-{}", self.rustc_channel),
            tool_version: self.rustc_version.clone(),
            confidence_level: ConfidenceLevel::High,
            assumptions: vec!["const fn restrictions guarantee termination".to_string()],
            evidence_type: EvidenceType::ImplicitTypeSystemGuarantee,
            evidence_location: None,
            date_verified: chrono::Utc::now(),
        }
    }

    /// Create auto trait annotation
    #[cfg(all(feature = "rust-ast", feature = "quote"))]
    fn auto_trait_annotation(&self, location: &Location, trait_path: &syn::Path) -> ProofAnnotation {
        let trait_name = quote::quote!(#trait_path).to_string();
        let property = match trait_name.as_str() {
            "Send" | "Sync" => PropertyType::ThreadSafety,
            _ => PropertyType::MemorySafety,
        };

        ProofAnnotation {
            annotation_id: crate::models::unified_ast::derive_annotation_id(
                &self.annotation_seed(location, &format!("AutoTrait/{trait_name}")),
            ),
            property_proven: property,
            specification_id: Some(format!("auto_trait_{trait_name}")),
            method: VerificationMethod::BorrowChecker,
            // "pmat-syn-static-analysis", not a compiler that never ran.
            tool_name: format!("pmat-{}", self.rustc_channel),
            tool_version: self.rustc_version.clone(),
            confidence_level: ConfidenceLevel::High,
            assumptions: vec![format!("{} auto trait implementation", trait_name)],
            evidence_type: EvidenceType::ImplicitTypeSystemGuarantee,
            evidence_location: None,
            date_verified: chrono::Utc::now(),
        }
    }

    /// Create auto trait annotation without quote
    #[cfg(all(feature = "rust-ast", not(feature = "quote")))]
    fn auto_trait_annotation(&self, location: &Location, trait_path: &syn::Path) -> ProofAnnotation {
        let trait_name = if let Some(segment) = trait_path.segments.last() {
            segment.ident.to_string()
        } else {
            "Unknown".to_string()
        };

        let property = match trait_name.as_str() {
            "Send" | "Sync" => PropertyType::ThreadSafety,
            _ => PropertyType::MemorySafety,
        };

        ProofAnnotation {
            annotation_id: crate::models::unified_ast::derive_annotation_id(
                &self.annotation_seed(location, &format!("AutoTrait/{trait_name}")),
            ),
            property_proven: property,
            specification_id: Some(format!("auto_trait_{}", trait_name)),
            method: VerificationMethod::BorrowChecker,
            // "pmat-syn-static-analysis", not a compiler that never ran.
            tool_name: format!("pmat-{}", self.rustc_channel),
            tool_version: self.rustc_version.clone(),
            confidence_level: ConfidenceLevel::High,
            assumptions: vec![format!("{} auto trait implementation", trait_name)],
            evidence_type: EvidenceType::ImplicitTypeSystemGuarantee,
            evidence_location: None,
            date_verified: chrono::Utc::now(),
        }
    }
}