Skip to main content

provable_contracts/query/
mod.rs

1//! Contract query engine with BM25 semantic search.
2//!
3//! Provides fast lookup across all contracts with semantic ranking,
4//! regex/literal search, and structured filters.
5//!
6//! Spec: `docs/specifications/sub/query.md`
7
8pub 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
29/// Execute a query against a contract index.
30pub fn execute(index: &ContractIndex, params: &QueryParams) -> QueryOutput {
31    let scored_indices = match params.mode {
32        SearchMode::Semantic => index.bm25_search(&params.query),
33        SearchMode::Regex => {
34            match index.regex_search(&params.query) {
35                Ok(idxs) => idxs.into_iter().map(|i| (i, 1.0)).collect(),
36                Err(_) => Vec::new(), // Invalid regex yields empty results
37            }
38        }
39        SearchMode::Literal => index
40            .literal_search(&params.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    // Build cross-project index lazily when any cross-project flag is set
56    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            // Go up from contracts/foo.yaml to the repo root
64            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
162/// Clean a contract path for display: strip to `contracts/...` relative form.
163fn clean_path(raw: &str) -> String {
164    // Use the last occurrence of "contracts/" to handle paths like
165    // /foo/contracts/crates/.../../../contracts/softmax-kernel-v1.yaml
166    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}