provable_contracts/query/
mod.rs1pub mod cross_project;
9mod index;
10mod persist;
11mod query_enrich;
12pub mod registry;
13mod types;
14mod types_render;
15
16pub use cross_project::CrossProjectIndex;
17pub use index::ContractIndex;
18pub use types::{
19 DiffInfo, EquationBinding, ProjectCoverage, ProofStatusInfo, QueryOutput, QueryParams,
20 QueryResult, ScoreInfo, SearchMode, ViolationInfo,
21};
22
23use crate::binding::BindingRegistry;
24use query_enrich::{
25 build_call_sites, build_coverage_map, build_violations, filter_by_project, filter_coverage,
26 filter_violations,
27};
28
29pub fn execute(index: &ContractIndex, params: &QueryParams) -> QueryOutput {
31 let scored_indices = match params.mode {
32 SearchMode::Semantic => index.bm25_search(¶ms.query),
33 SearchMode::Regex => {
34 match index.regex_search(¶ms.query) {
35 Ok(idxs) => idxs.into_iter().map(|i| (i, 1.0)).collect(),
36 Err(_) => Vec::new(), }
38 }
39 SearchMode::Literal => index
40 .literal_search(¶ms.query, params.case_sensitive)
41 .into_iter()
42 .map(|i| (i, 1.0))
43 .collect(),
44 };
45
46 let binding = params.binding_path.as_ref().and_then(|p| {
47 let content = std::fs::read_to_string(p).ok()?;
48 serde_yaml::from_str::<BindingRegistry>(&content).ok()
49 });
50
51 let filtered = apply_filters(index, scored_indices, params, binding.as_ref());
52 let total_matches = filtered.len();
53 let limited: Vec<_> = filtered.into_iter().take(params.limit).collect();
54
55 let needs_xp = params.show_call_sites
57 || params.show_violations
58 || params.show_coverage_map
59 || params.all_projects;
60 let xp_index = if needs_xp {
61 index.entries.first().map(|e| {
62 let p = std::path::Path::new(&e.path);
63 let contracts_dir = p.parent().unwrap_or(p);
65 let repo_root = if contracts_dir
66 .parent()
67 .is_none_or(|p| p.as_os_str().is_empty())
68 {
69 std::path::Path::new(".")
70 } else {
71 contracts_dir.parent().unwrap()
72 };
73 let extra = params.include_project.as_ref().map(std::path::Path::new);
74 cross_project::CrossProjectIndex::build_with_extra(repo_root, extra)
75 })
76 } else {
77 None
78 };
79
80 let project_filter = params.project_filter.as_deref();
81 let results: Vec<QueryResult> = limited
82 .into_iter()
83 .enumerate()
84 .map(|(rank, (idx, relevance))| {
85 build_result(
86 index,
87 params,
88 binding.as_ref(),
89 xp_index.as_ref(),
90 project_filter,
91 rank,
92 idx,
93 relevance,
94 )
95 })
96 .collect();
97
98 QueryOutput {
99 query: params.query.clone(),
100 total_matches,
101 results,
102 }
103}
104
105#[allow(clippy::too_many_arguments)]
106fn build_result(
107 index: &ContractIndex,
108 params: &QueryParams,
109 binding: Option<&BindingRegistry>,
110 xp_index: Option<&cross_project::CrossProjectIndex>,
111 project_filter: Option<&str>,
112 rank: usize,
113 idx: usize,
114 relevance: f64,
115) -> QueryResult {
116 let entry = &index.entries[idx];
117 let (depends_on, depended_by) = graph_fields(index, entry, params.show_graph);
118 QueryResult {
119 rank: rank + 1,
120 stem: entry.stem.clone(),
121 path: clean_path(&entry.path),
122 relevance,
123 description: entry.description.clone(),
124 kind: entry.kind,
125 equations: entry.equations.clone(),
126 obligation_count: entry.obligation_count,
127 references: opt_vec(&entry.references, params.show_paper),
128 depends_on,
129 depended_by,
130 score: params
131 .show_score
132 .then(|| query_enrich::build_score_info(entry))
133 .flatten(),
134 proof_status: params
135 .show_proof_status
136 .then(|| query_enrich::build_proof_status_info(entry))
137 .flatten(),
138 bindings: opt_binding(entry, binding, params.show_binding),
139 diff: params
140 .show_diff
141 .then(|| query_enrich::build_diff_info(entry))
142 .flatten(),
143 pagerank: if params.show_pagerank {
144 index.cached_pagerank(&entry.stem)
145 } else {
146 None
147 },
148 call_sites: filter_by_project(build_call_sites(&entry.stem, xp_index), project_filter),
149 violations: filter_violations(
150 build_violations(entry, xp_index, params.show_violations),
151 project_filter,
152 ),
153 coverage_map: filter_coverage(
154 build_coverage_map(&entry.stem, xp_index, params.show_coverage_map),
155 project_filter,
156 ),
157 }
158}
159
160fn clean_path(raw: &str) -> String {
162 if let Some(idx) = raw.rfind("contracts/") {
165 raw[idx..].to_string()
166 } else {
167 raw.to_string()
168 }
169}
170
171fn opt_vec(source: &[String], include: bool) -> Vec<String> {
172 if include {
173 source.to_vec()
174 } else {
175 Vec::new()
176 }
177}
178
179fn graph_fields(
180 index: &ContractIndex,
181 entry: &types::ContractEntry,
182 show: bool,
183) -> (Vec<String>, Vec<String>) {
184 if !show {
185 return (Vec::new(), Vec::new());
186 }
187 let deps = entry.depends_on.clone();
188 let rev = index
189 .depended_by(&entry.stem)
190 .into_iter()
191 .map(String::from)
192 .collect();
193 (deps, rev)
194}
195
196fn opt_binding(
197 entry: &types::ContractEntry,
198 binding: Option<&BindingRegistry>,
199 show: bool,
200) -> Vec<EquationBinding> {
201 if show {
202 query_enrich::build_binding_info(entry, binding)
203 } else {
204 Vec::new()
205 }
206}
207
208fn apply_filters(
209 index: &ContractIndex,
210 results: Vec<(usize, f64)>,
211 params: &QueryParams,
212 binding: Option<&BindingRegistry>,
213) -> Vec<(usize, f64)> {
214 results
215 .into_iter()
216 .filter(|(idx, _)| {
217 let entry = &index.entries[*idx];
218 filter_obligation(entry, params.obligation_filter.as_ref())
219 && filter_depends_on(entry, params.depends_on.as_ref())
220 && filter_depended_by(index, entry, params.depended_by.as_ref())
221 && filter_unproven(entry, params.unproven_only)
222 && filter_min_score(index, entry, params.min_score)
223 && filter_binding_gaps(entry, params.binding_gaps_only, binding)
224 && filter_min_level(entry, params.min_level.as_deref())
225 && filter_tier(entry, params.tier_filter)
226 && filter_class(entry, params.class_filter)
227 && filter_kind(entry, params.kind_filter)
228 })
229 .collect()
230}
231
232fn filter_kind(entry: &types::ContractEntry, kind: Option<crate::schema::ContractKind>) -> bool {
233 match kind {
234 Some(k) => entry.kind == k,
235 None => true,
236 }
237}
238
239fn filter_obligation(entry: &types::ContractEntry, obligation: Option<&String>) -> bool {
240 match obligation {
241 Some(ot) => entry.obligation_types.iter().any(|t| t == ot),
242 None => true,
243 }
244}
245
246fn filter_depends_on(entry: &types::ContractEntry, depends_on: Option<&String>) -> bool {
247 match depends_on {
248 Some(dep) => entry.depends_on.iter().any(|d| d == dep),
249 None => true,
250 }
251}
252
253fn filter_depended_by(
254 index: &ContractIndex,
255 entry: &types::ContractEntry,
256 depended_by: Option<&String>,
257) -> bool {
258 match depended_by {
259 Some(target) => index
260 .get_by_stem(target)
261 .is_some_and(|t| t.depends_on.contains(&entry.stem)),
262 None => true,
263 }
264}
265
266fn filter_min_score(
267 index: &ContractIndex,
268 entry: &types::ContractEntry,
269 min_score: Option<f64>,
270) -> bool {
271 let Some(threshold) = min_score else {
272 return true;
273 };
274 if let Some(cached) = index.cached_score(&entry.stem) {
275 return cached >= threshold;
276 }
277 query_enrich::build_score_info(entry).is_some_and(|s| s.composite >= threshold)
278}
279
280fn filter_binding_gaps(
281 entry: &types::ContractEntry,
282 gaps_only: bool,
283 binding: Option<&BindingRegistry>,
284) -> bool {
285 if !gaps_only {
286 return true;
287 }
288 let Some(binding) = binding else {
289 return false;
290 };
291 binding.bindings_for(&entry.stem).iter().any(|b| {
292 b.status == crate::binding::ImplStatus::NotImplemented
293 || b.status == crate::binding::ImplStatus::Partial
294 })
295}
296
297fn filter_unproven(entry: &types::ContractEntry, unproven_only: bool) -> bool {
298 if !unproven_only {
299 return true;
300 }
301 entry.obligation_count > entry.kani_count
302}
303
304fn filter_tier(entry: &types::ContractEntry, tier: Option<u8>) -> bool {
305 let Some(t) = tier else { return true };
306 registry::tier_of(&entry.stem) == t
307}
308
309fn filter_class(entry: &types::ContractEntry, class: Option<char>) -> bool {
310 let Some(c) = class else { return true };
311 registry::classes_of(&entry.stem).contains(&c)
312}
313
314fn filter_min_level(entry: &types::ContractEntry, min_level: Option<&str>) -> bool {
315 let Some(min) = min_level else { return true };
316 let threshold = query_enrich::parse_proof_level(min);
317 let path = std::path::Path::new(&entry.path);
318 let Ok(contract) = crate::schema::parse_contract(path) else {
319 return false;
320 };
321 let level = crate::proof_status::compute_proof_level(&contract, None);
322 level >= threshold
323}
324
325#[cfg(test)]
326mod tests {
327 include!("query_tests.rs");
328}
329#[cfg(test)]
330mod coverage_tests {
331 include!("query_tests_coverage.rs");
332}
333#[cfg(test)]
334mod render_tests {
335 include!("query_tests_render.rs");
336}