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
72 .parent()
73 .expect("parent is Some: the is_none_or branch above handles None")
74 };
75 let extra = params.include_project.as_ref().map(std::path::Path::new);
76 cross_project::CrossProjectIndex::build_with_extra(repo_root, extra)
77 })
78 } else {
79 None
80 };
81
82 let project_filter = params.project_filter.as_deref();
83 let results: Vec<QueryResult> = limited
84 .into_iter()
85 .enumerate()
86 .map(|(rank, (idx, relevance))| {
87 build_result(
88 index,
89 params,
90 binding.as_ref(),
91 xp_index.as_ref(),
92 project_filter,
93 rank,
94 idx,
95 relevance,
96 )
97 })
98 .collect();
99
100 QueryOutput {
101 query: params.query.clone(),
102 total_matches,
103 results,
104 }
105}
106
107#[allow(clippy::too_many_arguments)]
108fn build_result(
109 index: &ContractIndex,
110 params: &QueryParams,
111 binding: Option<&BindingRegistry>,
112 xp_index: Option<&cross_project::CrossProjectIndex>,
113 project_filter: Option<&str>,
114 rank: usize,
115 idx: usize,
116 relevance: f64,
117) -> QueryResult {
118 let entry = &index.entries[idx];
119 let (depends_on, depended_by) = graph_fields(index, entry, params.show_graph);
120 QueryResult {
121 rank: rank + 1,
122 stem: entry.stem.clone(),
123 path: clean_path(&entry.path),
124 relevance,
125 description: entry.description.clone(),
126 kind: entry.kind,
127 equations: entry.equations.clone(),
128 obligation_count: entry.obligation_count,
129 references: opt_vec(&entry.references, params.show_paper),
130 depends_on,
131 depended_by,
132 score: params
133 .show_score
134 .then(|| query_enrich::build_score_info(entry))
135 .flatten(),
136 proof_status: params
137 .show_proof_status
138 .then(|| query_enrich::build_proof_status_info(entry))
139 .flatten(),
140 bindings: opt_binding(entry, binding, params.show_binding),
141 diff: params
142 .show_diff
143 .then(|| query_enrich::build_diff_info(entry))
144 .flatten(),
145 pagerank: if params.show_pagerank {
146 index.cached_pagerank(&entry.stem)
147 } else {
148 None
149 },
150 call_sites: filter_by_project(build_call_sites(&entry.stem, xp_index), project_filter),
151 violations: filter_violations(
152 build_violations(entry, xp_index, params.show_violations),
153 project_filter,
154 ),
155 coverage_map: filter_coverage(
156 build_coverage_map(&entry.stem, xp_index, params.show_coverage_map),
157 project_filter,
158 ),
159 }
160}
161
162fn clean_path(raw: &str) -> String {
164 if let Some(idx) = raw.rfind("contracts/") {
167 raw[idx..].to_string()
168 } else {
169 raw.to_string()
170 }
171}
172
173fn opt_vec(source: &[String], include: bool) -> Vec<String> {
174 if include {
175 source.to_vec()
176 } else {
177 Vec::new()
178 }
179}
180
181fn graph_fields(
182 index: &ContractIndex,
183 entry: &types::ContractEntry,
184 show: bool,
185) -> (Vec<String>, Vec<String>) {
186 if !show {
187 return (Vec::new(), Vec::new());
188 }
189 let deps = entry.depends_on.clone();
190 let rev = index
191 .depended_by(&entry.stem)
192 .into_iter()
193 .map(String::from)
194 .collect();
195 (deps, rev)
196}
197
198fn opt_binding(
199 entry: &types::ContractEntry,
200 binding: Option<&BindingRegistry>,
201 show: bool,
202) -> Vec<EquationBinding> {
203 if show {
204 query_enrich::build_binding_info(entry, binding)
205 } else {
206 Vec::new()
207 }
208}
209
210fn apply_filters(
211 index: &ContractIndex,
212 results: Vec<(usize, f64)>,
213 params: &QueryParams,
214 binding: Option<&BindingRegistry>,
215) -> Vec<(usize, f64)> {
216 results
217 .into_iter()
218 .filter(|(idx, _)| {
219 let entry = &index.entries[*idx];
220 filter_obligation(entry, params.obligation_filter.as_ref())
221 && filter_depends_on(entry, params.depends_on.as_ref())
222 && filter_depended_by(index, entry, params.depended_by.as_ref())
223 && filter_unproven(entry, params.unproven_only)
224 && filter_min_score(index, entry, params.min_score)
225 && filter_binding_gaps(entry, params.binding_gaps_only, binding)
226 && filter_min_level(entry, params.min_level.as_deref())
227 && filter_tier(entry, params.tier_filter)
228 && filter_class(entry, params.class_filter)
229 && filter_kind(entry, params.kind_filter)
230 })
231 .collect()
232}
233
234fn filter_kind(entry: &types::ContractEntry, kind: Option<crate::schema::ContractKind>) -> bool {
235 match kind {
236 Some(k) => entry.kind == k,
237 None => true,
238 }
239}
240
241fn filter_obligation(entry: &types::ContractEntry, obligation: Option<&String>) -> bool {
242 match obligation {
243 Some(ot) => entry.obligation_types.iter().any(|t| t == ot),
244 None => true,
245 }
246}
247
248fn filter_depends_on(entry: &types::ContractEntry, depends_on: Option<&String>) -> bool {
249 match depends_on {
250 Some(dep) => entry.depends_on.iter().any(|d| d == dep),
251 None => true,
252 }
253}
254
255fn filter_depended_by(
256 index: &ContractIndex,
257 entry: &types::ContractEntry,
258 depended_by: Option<&String>,
259) -> bool {
260 match depended_by {
261 Some(target) => index
262 .get_by_stem(target)
263 .is_some_and(|t| t.depends_on.contains(&entry.stem)),
264 None => true,
265 }
266}
267
268fn filter_min_score(
269 index: &ContractIndex,
270 entry: &types::ContractEntry,
271 min_score: Option<f64>,
272) -> bool {
273 let Some(threshold) = min_score else {
274 return true;
275 };
276 if let Some(cached) = index.cached_score(&entry.stem) {
277 return cached >= threshold;
278 }
279 query_enrich::build_score_info(entry).is_some_and(|s| s.composite >= threshold)
280}
281
282fn filter_binding_gaps(
283 entry: &types::ContractEntry,
284 gaps_only: bool,
285 binding: Option<&BindingRegistry>,
286) -> bool {
287 if !gaps_only {
288 return true;
289 }
290 let Some(binding) = binding else {
291 return false;
292 };
293 binding.bindings_for(&entry.stem).iter().any(|b| {
294 b.status == crate::binding::ImplStatus::NotImplemented
295 || b.status == crate::binding::ImplStatus::Partial
296 })
297}
298
299fn filter_unproven(entry: &types::ContractEntry, unproven_only: bool) -> bool {
300 if !unproven_only {
301 return true;
302 }
303 entry.obligation_count > entry.kani_count
304}
305
306fn filter_tier(entry: &types::ContractEntry, tier: Option<u8>) -> bool {
307 let Some(t) = tier else { return true };
308 registry::tier_of(&entry.stem) == t
309}
310
311fn filter_class(entry: &types::ContractEntry, class: Option<char>) -> bool {
312 let Some(c) = class else { return true };
313 registry::classes_of(&entry.stem).contains(&c)
314}
315
316fn filter_min_level(entry: &types::ContractEntry, min_level: Option<&str>) -> bool {
317 let Some(min) = min_level else { return true };
318 let threshold = query_enrich::parse_proof_level(min);
319 let path = std::path::Path::new(&entry.path);
320 let Ok(contract) = crate::schema::parse_contract(path) else {
321 return false;
322 };
323 let level = crate::proof_status::compute_proof_level(&contract, None);
324 level >= threshold
325}
326
327#[cfg(test)]
328mod tests {
329 include!("query_tests.rs");
330}
331#[cfg(test)]
332mod coverage_tests {
333 include!("query_tests_coverage.rs");
334}
335#[cfg(test)]
336mod render_tests {
337 include!("query_tests_render.rs");
338}