provable_contracts/query/
types.rs

1//! Types for the contract query engine.
2
3use serde::{Deserialize, Serialize};
4
5/// How to interpret the query string.
6#[derive(Debug, Clone, PartialEq, Eq)]
7pub enum SearchMode {
8    /// BM25 semantic ranking over corpus (default).
9    Semantic,
10    /// Regex match against all string fields.
11    Regex,
12    /// Exact substring match (case-insensitive by default).
13    Literal,
14}
15
16/// A single entry in the contract index.
17#[derive(Debug, Clone, Serialize, Deserialize)]
18pub struct ContractEntry {
19    pub stem: String,
20    pub path: String,
21    pub description: String,
22    pub equations: Vec<String>,
23    pub obligation_types: Vec<String>,
24    pub properties: Vec<String>,
25    pub references: Vec<String>,
26    pub depends_on: Vec<String>,
27    pub is_registry: bool,
28    pub obligation_count: usize,
29    pub falsification_count: usize,
30    pub kani_count: usize,
31    /// Concatenated searchable text for BM25.
32    pub corpus_text: String,
33}
34
35/// Parameters controlling a query.
36#[derive(Debug, Clone)]
37#[allow(clippy::struct_excessive_bools)]
38pub struct QueryParams {
39    pub query: String,
40    pub mode: SearchMode,
41    pub case_sensitive: bool,
42    pub limit: usize,
43    pub obligation_filter: Option<String>,
44    pub min_score: Option<f64>,
45    pub depends_on: Option<String>,
46    pub depended_by: Option<String>,
47    pub unproven_only: bool,
48    pub show_score: bool,
49    pub show_graph: bool,
50    pub show_paper: bool,
51    pub show_proof_status: bool,
52    pub show_binding: bool,
53    pub binding_path: Option<String>,
54    pub binding_gaps_only: bool,
55    pub show_diff: bool,
56    pub show_pagerank: bool,
57    pub show_call_sites: bool,
58    pub show_violations: bool,
59    pub show_coverage_map: bool,
60    pub min_level: Option<String>,
61    /// Filter cross-project results to a named project (e.g., "aprender").
62    pub project_filter: Option<String>,
63    /// Explicit additional project path to include in cross-project scan.
64    pub include_project: Option<String>,
65    /// Force cross-project scan even when no cross-project flags are set.
66    pub all_projects: bool,
67    /// Filter by contract tier (1-7).
68    pub tier_filter: Option<u8>,
69    /// Filter by kernel equivalence class (A-E).
70    pub class_filter: Option<char>,
71}
72
73impl Default for QueryParams {
74    fn default() -> Self {
75        Self {
76            query: String::new(),
77            mode: SearchMode::Semantic,
78            case_sensitive: false,
79            limit: 10,
80            obligation_filter: None,
81            min_score: None,
82            depends_on: None,
83            depended_by: None,
84            unproven_only: false,
85            show_score: false,
86            show_graph: false,
87            show_paper: false,
88            show_proof_status: false,
89            show_binding: false,
90            binding_path: None,
91            binding_gaps_only: false,
92            show_diff: false,
93            show_pagerank: false,
94            show_call_sites: false,
95            show_violations: false,
96            show_coverage_map: false,
97            min_level: None,
98            project_filter: None,
99            include_project: None,
100            all_projects: false,
101            tier_filter: None,
102            class_filter: None,
103        }
104    }
105}
106
107/// A single query result with relevance score and optional enrichment.
108#[derive(Debug, Clone, Serialize)]
109pub struct QueryResult {
110    pub rank: usize,
111    pub stem: String,
112    pub path: String,
113    pub relevance: f64,
114    pub description: String,
115    pub equations: Vec<String>,
116    pub obligation_count: usize,
117    pub references: Vec<String>,
118    pub depends_on: Vec<String>,
119    #[serde(skip_serializing_if = "Vec::is_empty")]
120    pub depended_by: Vec<String>,
121    #[serde(skip_serializing_if = "Option::is_none")]
122    pub score: Option<ScoreInfo>,
123    #[serde(skip_serializing_if = "Option::is_none")]
124    pub proof_status: Option<ProofStatusInfo>,
125    #[serde(skip_serializing_if = "Vec::is_empty")]
126    pub bindings: Vec<EquationBinding>,
127    #[serde(skip_serializing_if = "Option::is_none")]
128    pub diff: Option<DiffInfo>,
129    #[serde(skip_serializing_if = "Option::is_none")]
130    pub pagerank: Option<f64>,
131    #[serde(skip_serializing_if = "Vec::is_empty")]
132    pub call_sites: Vec<CallSiteInfo>,
133    #[serde(skip_serializing_if = "Vec::is_empty")]
134    pub violations: Vec<ViolationInfo>,
135    #[serde(skip_serializing_if = "Vec::is_empty")]
136    pub coverage_map: Vec<ProjectCoverage>,
137}
138
139/// Cross-project call site for a contract.
140#[derive(Debug, Clone, Serialize)]
141pub struct CallSiteInfo {
142    pub project: String,
143    pub file: String,
144    pub line: u32,
145    pub equation: Option<String>,
146}
147
148/// A contract violation detected in a consumer project.
149#[derive(Debug, Clone, Serialize)]
150pub struct ViolationInfo {
151    pub project: String,
152    pub kind: String,
153    pub detail: String,
154}
155
156/// Per-project coverage summary for a contract.
157#[derive(Debug, Clone, Serialize)]
158pub struct ProjectCoverage {
159    pub project: String,
160    pub call_sites: usize,
161    pub binding_refs: usize,
162    pub binding_implemented: usize,
163    pub binding_total: usize,
164}
165
166/// Inline score info for enrichment.
167#[derive(Debug, Clone, Serialize)]
168pub struct ScoreInfo {
169    pub composite: f64,
170    pub grade: String,
171    pub spec_depth: f64,
172    pub falsification: f64,
173    pub kani: f64,
174    pub lean: f64,
175    pub binding: f64,
176}
177
178/// Inline proof status info for enrichment.
179#[derive(Debug, Clone, Serialize)]
180pub struct ProofStatusInfo {
181    pub level: String,
182    pub obligations: u32,
183    pub falsification_tests: u32,
184    pub kani_harnesses: u32,
185    pub lean_proved: u32,
186}
187
188/// Git diff summary for a contract.
189#[derive(Debug, Clone, Serialize)]
190pub struct DiffInfo {
191    pub last_modified: String,
192    pub days_ago: u64,
193    pub commit_hash: String,
194}
195
196/// Binding status for a single equation.
197#[derive(Debug, Clone, Serialize)]
198pub struct EquationBinding {
199    pub equation: String,
200    pub status: String,
201    #[serde(skip_serializing_if = "Option::is_none")]
202    pub module_path: Option<String>,
203}
204
205/// Output of a query execution.
206#[derive(Debug, Clone, Serialize)]
207pub struct QueryOutput {
208    pub query: String,
209    pub total_matches: usize,
210    pub results: Vec<QueryResult>,
211}
provable_contracts/query/types.rs

provable_contracts/query/
types.rs
